COMMON DERIVATIONS IN LOCALLY DETERMINED
NONMONOTONIC RULE SYSTEMS AND THEIR COMPLEXITY
By
AMY K. C. S. VANDERBILT
A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL
OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT
OF THE REQUIREMENTS FOR THE DEGREE OF
DOCTOR OF PHILOSOPHY
UNIVERSITY OF FLORIDA
2000
I dedicate this dissertation to the memory of Sara Davidson Sartain, who put
her foot down. Most importantly, I dedicate it to Scott and Sabrina, for whom I
would accomplish anything and with whom I could accomplish anything.
ACKNOWLEDGMENTS
I would like to thank the University of Florida and the Department of Math-
ematics for their encouragement and contributions to my education, experience, and
funding. Special and heart-felt thanks go to my committee, who from the first day
were supportive and helpful above and beyond the call of duty. Thanks to my parents,
Ronald and Linda Sartain, without whom I might never have taken my education this
far and without whom I might never have gone to conferences! An enormous thanks
to my advisor, Dr. Douglas A. Cenzer, who not only put up with me for these years,
but encouraged my tenacious approach and worked to help me achieve my goals, both
for this dissertation and for the years beyond. Lastly, the greatest thanks go to my
husband, Scott, for constant encouragement and support (and chocolate pie!), and
to my daughter, Sabrina, who (although not around for the entire undertaking) was
there with daily hugs and smiles and reminders of what life is really about.
in
TABLE OF CONTENTS
pa g e
ACKNOWLEDGEMENTS iii
ABSTRACT vi
1 INTRODUCTION 1
1.1 History 1
1 .2 Motivation 3
1 .3 Preliminary Theorems and Definitions: Nonmonotonic Rule
Systems 5
1 .4 Common Derivations in Locally Determined Systems 16
2 THE FINITE CASE 18
2.1 Finite Classical Nonmonotonic Rule Systems 18
2.2 Finite Constructive Nonmonotonic Rule Systems 32
2.3 Characterizing the Set of Extensions 36
3 THE INFINITE CASE 38
3 . 1 Locally Finite Classical Nonmonotonic Rule Systems 38
3 .2 Locally Finite Constructive Nonmonotonic Rule Systems 51
3.3 Characterizing The Set of Extensions 59
4 LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS 60
4. 1 Locally Determined Nonmonotonic Rule Systems 60
4.2 Common Derivations in Locally Determined Nonmonotonic
Rule Systems 67
4.3 Characterizing the Set of Extensions 69
5 COMPUT ABILITY AND COMPLEXITY ISSUES 76
5.1 Finding Extensions with Low Complexity 76
5.2 Computability and Complexity of Common Derivations 82
IV
6 ALTERNATE FORMALISMS OF NONMONOTONIC LOGIC 86
6.1 Default Logic: Preliminary Definitions and Theorems 86
6.2 Equivalence of Default Logic to Nonmonotonic Rule Systems 90
6.3 Previous Results Through the Eyes of Default Logic 91
6.4 Logic Programming: Preliminary Definitions and Theorems 114
6.5 Equivalence of Logic Programming to Nonmonotonic
Rule Systems 120
6.6 Previous Results Through the Eyes of Logic Programming 121
7 FUTURE DIRECTIONS 131
REFERENCES 133
BIOGRAPHICAL SKETCH 137
Abstract of Dissertation Presented to the Graduate School
of the University of Florida in Partial Fulfillment of the
Requirements for the Degree of Doctor of Philosophy
COMMON DERIVATIONS IN LOCALLY DETERMINED
NONMONOTONIC RULE SYSTEMS AND THEIR COMPLEXITY
By
Amy K. C. S. Vanderbilt
May 2000
Chairman: Douglas Cenzer
Major Department: Mathematics
Nonmonotonic Rule Systems are a general framework for commonsense rea-
soning. U =< U,N > is a nonmonotonic rule system where the universe U is a
countable set, such as the set of sentences of some propositional logic; N is a set of
rules of inference under which a conclusion from U may be inferred from the pres-
ence of premises and the absence of restraints. An extension of U is a set of beliefs
concurrent with the rules of inference. If <j> is a formula of the language, appearing
in every extension of < U, N >, then <\> has a common derivation d 1 ^ that gener-
ates (j) in every extension. Further, every extension of < U, N > is an extension of
< U, N U {d l <p} >. These two sets of extensions may be equal, but this is not al-
ways true. A constructive view enhances as well as simplifies the results. We explore
alternate forms of the common derivation d that ensure certain properties for the re-
sulting nonmonotonic rule system < U, N U {d} > . We then introduce the notion of
levels and locally determined systems. The previous questions are explored in terms
VI
of these systems. Computability and complexity issues of the common derivations
are considered. Several conditions are detailed, based on the notion of levels, which
ensure that a nonmonotonic rule system will have a computable extension. These
results are refined to give conditions which ensure the existence of extensions of low
complexity (such as exponential time). If U is a recursive nonmonotonic rule system
with (effective) levels, there is a 1:1 degree preserving correspondence between the set
of extensions of U and the set of paths through a recursive finitely branching (highly
recursive) tree. The families of extensions of a nonmonotonic rule system with levels
are characterized. We find that for any closed (Ilf) family S of subsets of U having
levels, there exists a (recursive) nonmonotonic rule system U with (recursive) levels
such that S is the set of extensions of U.
vii
CHAPTER 1
INTRODUCTION
In this chapter, we provide a motivation for the directions of the research as
well as necessary background definitions and preliminary theorems. Along with this,
we take a short exploration of the history of the subject and of the directions research
in the field is presently taking.
1.1 History
In mathematics, a conclusion drawn from a set of axioms can also be drawn
from any larger set of axioms containing the original set. The deduction remains
no matter how the axioms are increased. This is monotonic reasoning in that new
information does not affect the conclusions drawn from a set of premises. From the
time of Euclid, it has been the nature of this monotonic reasoning that makes math-
ematical proofs permanent. Complete proofs of theorems are never later withdrawn
due to new information.
There is, however, another sort of reasoning that is not monotonic. In this
type of reasoning, we deduce a statement based on the absence of any evidence to
the contrary. Such a statement is therefore more of a belief than a truth, as we may
later come upon new information that contradicts the statement. Statistics is often
used as a tool for for deducing provisional beliefs, but not every problem comes with
its own set of distributions ready for use.
Such deductions may arise in situations where we are made to choose con-
cretely between two actions in the absence of complete information. It may be that
we cannot wait for the complete information to show itself, or that we have no guar-
antee that it will ever show itself. Thus beliefs are often accepted as truth based on
a lack of contradicting facts.
One of the standard illustrations of this commonsense reasoning is the "Tweety"
example. If we see only birds that can fly, then we deduce that birds can fly. If Tweety
is a bird, we conclude that Tweety can fly. If we later find that Tweety is a penguin,
then we are forced to retract our conclusion that Tweety can fly. We are back to
knowing only that Tweety is a bird, specifically a penguin.
Every vision of a nonmonotonic logic describing belief will be similar, depend-
ing only on our definition of a lack of evidence against a conclusion. McCarthy [1980]
was one of several who initiated formalizations of nonmonotonic logic with his concept
of Circumscription. At the same time, Reiter [Rei80] created a formalization that
he termed Default Logic. Along with these are the Theory of Multiple Believers of
Hintikka (1962), the Truth Maintenance Systems of Doyle [Do79], the Autoepistemic
Logic of Moore (1985), the Theory of Individual and Common Knowledge and Belief
of Halpern and Moses (1984), and Logic Programming with Negation as Failure given
by Apt (1988). This is only a partial list. The first journeys into the nonmonotonic
aspects of logic can be traced to Reiter's Default Logic [Rei80]. This involved creating
a natural extension of classical logic that would easily handle negative information.
These nonmonotonic logics share many properties. Several translations be-
tween them have been made by Konolige (1988), Gelfond and Przymusihska (1986,
1989), Reinfrank and Dressier (1989), and Marek and Truszczyhski (1989). It should
be noted that these translations are primarily for propositional logic.
Apt [A90], and Gelfond and Lifschitz [GL88] studied negation as failure in
logic programming. It has since been seen that each of these investigations were
in a common direction. Relationships were discovered by several, including Marek
and Trusczcynski (1989), who explored the precise nature of the connections between
Default Logic and Logic Programming.
Since then, many aspects of the computability and complexity of the exten-
sions of these systems have been explored. Subsequently, algorithms for computing
the extensions of any one theory have been created. More importantly, a universal
system of nonmonotonic logic called Nonmonotonic Rule Systems was created by
Marek, Nerode, and Remmel [MNR90 and MNR92a]. This system has been shown
by Marek, Nerode, and Remmel and others to be equivalent to many other systems of
nonmonotonic logic including Reiter's Default Logic as well as Logic Programming,
and Modal Nonmonotonic Logic.
1.2 Motivation
We suppose that we have a sentence (j) appearing in some or all extensions
of a nonmonotonic rule system. We want to then construct a single rule that would
derive 4> in every extension of the system. The motivation behind this "common
derivation" is that it would tell us what is required, in a nutshell, to derive <j> in
this system. Nonmonotonic Logic has a place in fields such as medicine and political
science where this kind of information would be useful.
In the world of medical diagnoses, we imagine that our system involves a
universe U of symptoms to be matched with a diagnosis. We would care to know
a concise list of what symptoms should be present and, just as importantly, what
symptoms should be absent in order to accurately diagnose a condition.
My ultimate goal is to manipulate Nonmonotonic Rule Systems to create a
mathematical system which would lend itself to applications in political science (and
possibly social science as a whole as well as advertising) and explore the subsequent
theory of that system.
First Order Logic is inherently monotonic. Human reasoning, however, in-
volves not only the addition of beliefs, but the retraction of beliefs, based on new
information, i.e. it is nonmonotonic. For example, the study of Astronomy led to the
retraction of the belief of a geocentric universe. Thus, to formalize human reasoning,
a nonmonotonic logic is needed. I propose to consider Political Science as an area of
future application. This area is ripe for the use of Nonmonotonic Logic since Political
Science studies how groups of people react to a campaign and how they reason who
they will vote for. If human reasoning can be formalized, then the reasoning of the
electorate can be modeled.
Other types of mathematics used to model the electorate in the past include
statistics, game theory [Gol94] and measure theory [B90]. Some of these models
managed to get as accurate as 84 percent [Gol94], but had to be redone every time a
subset of the electorate changed its mind (which was often!). Secondly, the accuracy
of the model was only known after the election was already over. These two properties
made the models unreliable and expensive. The problem: these types of mathematics
are monotonic, so the conclusions they reach cannot be retracted upon receipt of new
information.
We imagine that we create one nonmonotonic rule system per category of
voters and we consider the extensions of each theory or system. We would like all
the extensions for a category to contain some conclusion such as, "I will vote for
candidate A." For this reason, we take great interest not only in the intersections of
extensions, but also in the process of deduction used to create those extensions. It is
for this reason that we explore the concept of a common derivation for a conclusion
that appears in some or all extensions. Having one rule that derives the conclusion
"I will vote for candidate A" in each extension allows us to see exactly what must be
concluded previously and what must not have been concluded in order to allow the
derivation to apply.
1.3 Preliminary Theorems and Definitions: Nonmonotonic Rule Systems
The following background is taken from Marek, Nerode, and Remmel's series
of papers [MNR90] and [MNR92a]. Here we introduce the notion of a nonmonotonic
formal system < U, N >.
Definition 1.3.1 A NONMONOTONIC RULE OF INFERENCE is a triple <P,R,d>>,
where P = {a>i,...,a n }, and R = {/?i,...,/? m } are finite lists of objects from U and
4> G U. Each such rule is written in the form r = a\,...,a n : /3 1} ...,/3 m /0. Here
{a\,...,a n } are called the PREMISES of the rule r, {/?i,...,/? m } are called the RE-
STRAINTS of the rule r, and cln(r) = c{r) = </> is the CONCLUSION ofr.
Either P or R or both may be empty. If R is empty, then the rule is monotonic.
In the case that both P and R are empty, we call the rule r an axiom. For a set A
of rules, let c(A) = {c(r)\r e A}.
A NONMONOTONIC FORMAL SYSTEM is a pair <U,N>, where U is a
nonempty set and N is a set of nonmonotonic rules. Each monotonic formal system
can be identified with the nonmonotonic formal system in which every monotonic
rule is given an empty set of restraints. The standard example for U will be the
set Sent(V) of propositional sentences on a finite or countable set of propositional
variables (or atoms). Here we will frequently assume that the standard propositional
rules of deduction are implicitly included as monotonic rules in any nonmonotonic
rule system with universe U. In the constructive case, a proper subset of these rules
are assumed.
Now, if < U, N > is a nonmonotonic rule system, and 5 is a set of formulas
of the language, call a rule r <E N GENERATING FOR THE CONTEXT S if the
premises of r are in S, and no element of the restraints is in S. Let GD(N, S) be the
set of all rules in N that generate for the context S.
6
A subset S C U is called DEDUCTIVELY CLOSED if for every rule r £ N,
we have that if all premises {ai,...,a n } are in S and all restraints {/?i,..., /3 m } are not
in S then the conclusion belongs to 5.
In nonmonotonic rule systems, deductively closed sets are not generally closed
under arbitrary intersections as in the monotone case. But deductively closed sets are
closed under intersections of descending chains. Since U is deductively closed, by the
Kuratowski-Zorn Lemma, any / C U is contained in at least one minimal deductively
closed set. The intersection of all the deductively closed sets containing / is called
the set of SECURED CONSEQUENCES of /. This set is also the intersection of all
minimal deductively closed sets containing /. Deductively closed sets are thought of
as representing possible "points of view." the intersection of all deductively closed
sets containing / represents the common information present in all such "points of
view" containing /.
Example 1.3.1 Let U = {a,b,c}.
(a) Consider U with Ni = {: /a; a : — >6/6} . There is only one minimal
deductively closed set S — {a, b}. Then S is the set of secured consequences of
<U,N X >.
(b) Consider U with N 2 = {: / o; a : b/c; a : c/b). Then there are two minimal
deductively closed sets, S x = {a,b} and S 2 = {a,c}. The singleton set {a} is the set
of secured consequences of < U, N 2 > .
Part (b) of this example shows that the set of all secured consequences is not,
in general, deductively closed in the nonmonotone case. Note that if we implicitly
assume the rules of propositional logic we define Cn(S) to be the closure of the set
S under these implicit monotonic rules
Given a set S and an / C U, and 5-DERIVATION of </> from / in the system
< U, N > is a finite sequence < 0!,...,^ > such that <f> k = cf> and, for all i < k,
each 0i is in /, or is an axiom, or is the conclusion of a rule r e N such that all the
premises of r are included in {(fii,..., <j>i-\) and all restraints of r are in U — S. An S-
CONSEQUENCE of I is an element of U occurring in some 5-deduction from /. Let
Cs{I) be the set of all S-consequences of / in < U, N >. I is a subset of Cs(I). Note
that S enters solely as a restraint on the use of the rules imposed by the restraints
in the rules. A single restraint in a rule in N may be in S and therefore prevent the
rule from ever being applied in an 5-deduction from /, even though all the premises
of that rule occur earlier in the deduction. Thus, S contributes no members directly
to Cs(I), although members of S may turn up in Cs{I) by an application of a rule
which happens to have its conclusion in S. For a fixed S, the operator Cs(*) is
monotonic. That is, if IC J, then C S (I) C C S (J). Also, C S (C S {I)) = C S (I).
Generally, Cs(I) is not deductively closed in < U, N >. It is possible that all
the premises of a rule be in Cs(I), the restraints of that rule are outside of Cs(I),
but a restraint of that rule be in 5, preventing the conclusion from being put into
Cs(I).
Example 1.3.2 Let U = {a,b,c},N = {: /a;a: b/c}, and S = {b}. Then, C s (0) ■
{a} is not deductively closed.
However, we do get the following result:
Theorem 1.3.2 (MNR90) If S C C S {I) then C S (I) is deductively closed.
We say that S C U is an EXTENSION of / if C S (I) = S.
S is an extension of / if two things happen. First, every element of S is
deducible from /, that is, S C C S (I) (this is the analogue of the adequacy property
in logical calculi). Second, the converse holds: all the 5-consequences of / belong to
S (this is the analogue of completeness).
In purely monotonic rule systems, extensions usually refer to larger theories
(under inclusion). This is definitely not the meaning of extension for nonmonotonic
rule systems. In fact, it will be seen that for any two extensions A and B of a
nonmonotonic rule system, it is never the case that A C B. An important family in
propositional logic is the set of complete consistent extensions, CCE(T), of a theory
T. Any such family can be obtained as the set of extensions of a nonmonotonic
rule system. We obtain this system by taking the monotonic rules as restraint-free
nonmonotonic rules and adding rules of the form : (j>/-<<j) and : ->0/</>, for each sentence
4> (to secure completeness).
The notion of an extension is related to that of a minimal deductively closed
set.
Theorem 1.3.3 (MNR90) // S is an extension of I, then: (1) S is a minimal
deductively closed superset of I. (2) For every V such that I C /' C S, Cs(I') = S.
Example 1.3.3 Let a, b, and c be atoms in the language L and let
U = {a,b,c}
and
iV = {:{a}/6,:{c}/6,:{a}/c,:{c}/a}.
Then the nonmonotonic rule system < U,N > has two extensions:
5i = {6,c}
and
Moreover, we find that
S 2 = {b,a}.
GD(N,S 1 ) = {:{a}/b,:{a}/c}
and
GD(N,S 2 ) = {:{c}/b,:{c}/a}.
Now, we may well-order the rules of a nonmonotonic rule system < U, N > by
some well-ordering < We may then define AD^. to be the set of all rules in TV which
are applied when the well-ordering is used to close under the set of rules. This is
done in the following way: we define an ordinal tfc. For every e < 77^ we define a set
of rules AD £ and a rule r e . If the sets AD £ , e < a, have been defined but 77^ has not
been defined, then a rule r is applicable at stage a if the following two conditions
hold:
(*)c(U t<a AD t )\-P(r)
( b ) c(U £ <a AD e ) \f (3, for every € R(r).
(1) If there is no applicable rule r £ N\ [) £<a AD £ , then r^ = a and AD Q =
(2) Otherwise, define r Q to be the ^-least applicable rule r e N\ \J £<Q AD e
and set AD a = (|J e<a AD,) U{r a }.
(3) Put AD± = U £< ^ AD S .
Intuitively, we begin with the empty set of formulas and apply the rules of TV
in their order. Each time we apply only the ordering-least rule which can be applied.
At some point (since the ordinal is well-defined [MT93a]) there will be no available
rules that may be applied. At this point, AD± is the set of all rules applied and r^
is the number of steps needed to reach this stopping point.
Then, let T± be c(AD^). This is the theory GENERATED BY < Then,
GD(N,T^) CAD± so that
c(GD(N,T±))CT±.
10
Now, if X is a well-ordering of the rules and for every /? in R(AD^), (5 £ c(AD^)
then T-< is an extension of < U, N >. That is, if
AD± = GD(N,T±),
then
T± = c(AD^)
is an extension of < U, N >. More precisely, if 71< = c(GD(N,T±)), then T< is an
extension of < U, N > . We now have that
(a) [MT93a] If S is an extension of < U, N > then there is some well-ordering
^ of the rules in N such that
S = c(AD±) = c{GD{N,S)).
And,
(b) US = T^ = c(AD^) = c(GD(N,S)) for some well-ordering <, then S is
an extension of < U, N > .
Thus, S is an extension of < U, N > if and only if S = c(GD(N, S)).
It is important to note that a well-ordering may not give rise to an extension.
The new rule r Q may have a conclusion that contradicts the restraint of a previously
applied rule. Then, T-< is not an extension. Consider the following example:
Example 1.3.4 Let < U,N > be the nonmonotonic rule system where U = {a,b}
and N = {: {a}/b; b : /a}. Then rule r x is applicable at stage one. At stage two, rule
r 2 is applicable; however, the conclusion of r 2 violates the restraint of r l . Thus, this
system has no extensions.
Thus, we must concede that if c((J £<Q AD e ) h (3, where /? € R(r) for some
rule r € [j e<a AD e , then the well-ordering does not define an extension.
11
Let £(< U,N >) be the set of all extensions of the nonmonotonic rule system
<U,N >. Call two nonmonotonic rule systems <U\,Ni> and < U 2 , N 2 > EQUIV-
ALENT, written < Ui,N\ >=< U 2 , N 2 >, if they have exactly the same extensions,
i.e., if £{< U u Ni >) = £(< U 2 ,N 2 >) [MT93a].
Example 1.3.5 Let < U,N > be a nonmonotonic rule system where U = {a, b},
and N\ = {: /a;a : /b}. Then consider the nonmonotonic rule system < U, N 2 >
where N 2 = {: /b;b : /a). These two theories are equivalent as they each have the
same single extension
S = {a,b}.
Theorem 1.3.4 (MT93) A nonmonotonic rule system <U,N > has an inconsis-
tent extension if and only if Sent(L) is an extension and < U,N > has no other
extensions.
Theorem 1.3.5 (MNR90) The set of extensions of a nonmonotonic rule system
forms an antichain. That is, if S\ , S 2 are extensions of a nonmonotonic rule system
<U,N > and Si C S 2 , then S x = S 2 .
Though this is a widely known fact about all forms of nonmonotonic logic,
this is an important concept for the characterization of the family of extensions of a
nonmonotonic rule system The natural question here is under what conditions is an
antichain the set of extensions of a nonmonotonic rule system? Consider the following
example:
Example 1.3.6 Considering the monotonic theory T = Cn(a — ► b) and the set
V = {a, 6} of atoms. The set of complete consistent extensions of this monotonic
12
theory can be seen as the set of extensions of the nonmonotonic rule system < V, N >
where N = {: ->a/a; : a/->a; : — >6/6; : b/-<b; a : /b}. This system has three extensions:
S 1 = Gn({a,6}),
S 2 = Cn({^a,b}),
and
S 3 = Cn({^a,^b}).
It will not always be so easy to construct a nonmonotonic rule system whose
extensions are exactly what we want them to be. We address this in detatil in
subsequent chapters.
Next we need to define the notions of recursive and highly recursive non-
monotonic rule systems < U,N >. Without loss of generality, we may assume that
U C u and we will identify a rule r = ai,...,a n : /? lv ..,/? m /0 in N with its code
c(r) =< k,l,<j>> where D k = {a u ...,a n } and D t = {/?i,...,/J m }. In this way, we can
think of iV as a subset of a;. We say that a nonmonotonic rule system < U, N > is
RECURSIVE if both U and N are recursive subsets of w. To define the notion of
a highly recursive nonmonotonic rule system < U, N >, we must first introduce the
concept of a PROOF SCHEME for in < U, N >.
A proof scheme for is a finite sequence p =<< <j> Q ,ro,can(G ) >,...,<
^m,?"m,con(G m ) >> such that <f> m = <f> and
(1) If m = then: (a) O is an axiom (that is, there exists a rule r g N,r =:
M>), r o = r > and G = or (b) is a conclusion of a rule r =: 0t,..., /3 T , r = r, and
Go = {A, •.,&}•
(2) m > 0, << o ,r o ,can(Go) >,...,< <^ m _i,r m _ 1 ,can(G m _ 1 ) >> is a proof
scheme of length m and <j> m is a conclusion of r = ^ io ,...,^ : p u ..., /3 r /(t) m where
to,..., i s <m,r m = r, and G m = G m _i U {A,..., /? r }.
13
The formula m is called the CONCLUSION of the proof scheme p and denoted
by cln(p), the set G m is called the SUPPORT of p and is denoted by supp(p).
The idea behind this concept is this: any 5-derivation, p, in the system U =<
U,N >, uses some negative information about S to ensure that the restraints of rules
that were used are outside of S. But this negative information is finite, that is, it
involves a finte subset of the complement of 5, such that as long as G fl S\ = 0, p
is an Si-derivation as well. In the notion of proof scheme we capture this finitary
character of the 5-derivation.
A proof scheme with the conclusion </> may include a number of rules that are
irrelevant to the enterprise of deriving <f>. There is a natural preordering on proof
schemes. Namely, we say that p < p\ if every rule appearing in p also appears in p x .
The relation is not a partial ordering, and it is not a partial ordering if we restrict
ourselves to proof schemes with a fixed conclusion </>. Yet it is a well-founded relation,
namely, for every proof scheme p there exists a MINIMAL PROOF SCHEME p\ <p
[e.g. q is minimal if for every p 2 , if p<i -< q, then q -< p 2 ] moreover, we can, if desired,
require the conclusion of p x to be the same as that of p.
We also set p = pi equivalent to p -< p x A p\ < p and see that = is an
equivalence relation and that its equivalence classes are finite.
We say that the nonmonotonic rule system < U, N > is LOCALLY FINITE if
for every $€U there are finitely many -<-minimal proof schemes with conclusion <j>.
This concept is motivated by the fact that, for locally finite systems, for every there
is a finite set, Dr^, of derivations such that all the derivations of are inessential
extensions of derivations in Dr^. That is, if p is a derivation of 0, then there is a
derivation p x e Dr^ such that p x -< p. Finally, we say that the system < U, N > is
HIGHLY RECURSIVE if it is recursive, locally finite, and the map — ► can{Dr^)
is partial recursive. That is, there exists an effective procedure which, given any
14
4> 6 U, produces a canonical index of the set of all -<-minimal proof schemes with
conclusion (j>. We let £(< U, N >) denote the set of extensions of the system.
For a nonmonotonic rule system < U, N >, define a rule r to be RESTRAINT-
FREE if its set of restraints is empty. Define a sentence <\> G U to be TERMINALLY
RESTRAINT-FREE if the last rule in each of its minimal proof schemes is restraint
free. Define a subset A of U to be terminally restraint-free if every sentence <j) G A is
terminally restraint free.
Definition 1.3.6 For a nonmonotonic rule system < U,N >, define a sentence
4> G U to be PREMISE-FREE if each of its minimal proof schemes has length one.
Define a subset A of U to be premise-free if every sentence (j) G A is premise-free.
Definition 1.3.7 For a nonmonotonic rule system < U,N >, define a rule r to
be NORMAL if the set of restraints consists only of the negation of the conclusion.
Define a sentence (j> G U to be TERMINALLY NORMAL if the last rule in each of
its minimal proof schemes is normal. Define a subset A of U to be terminally normal
if every sentence (f> G A is terminally normal.
To consider the relationship between sets of extensions and trees, we will need
the following background, as given by Cenzer and Remmel [CR99].
Let u = {0,1,2,...} denote the set of natural numbers and let <,>: u x
w — > u be some fixed one-to-one and onto recursive pairing function such that the
projection functions 7Ti and n 2 defined by 7T!(< x,y >) = x and 7r 2 (< x,y >) = y
are also recursive. We extend our pairing function to code n-tuples for n > 2 by the
usual inductive definition, that is < Xi,...,x„ >=< x x , < x 2 ,...,x n » for n i 2. We
let a; <tJ denote the set of all finite sequences from u and 2 <UJ denote the set of all
finite sequences of 0's and l's. Given a =< a>i,...,a n > and =< (5 U ... , (3 k > in
uj <uj we write a Q (5 if o: is an initial segment of /?. Now we can identify a sequence
15
a =< a lr .., a n > with its code c(a) =< n, < tti,..., a n >> in u>. We let be the code
of the empty sequence 0. Thus, when we say a set 5 C u> <u) is recursive or recursively
enumerable, we mean the set {c(oj)|o; G S} is recursive or recursively enumerable. A
TREE T is a nonempty subset of cj <w such that T is closed under initial segments. A
function / : u — ► w is an infinite PATH through T if for all n, < /(0),..., f(n) >G T.
We let P(T) denote the set of all paths through T. A set A of functions is a II ! class
if there is a recursive predicate R such that A — {/ G w w |(Vn), R(< /(0),...,/(n) >)}.
A n°i class is RECURSIVELY BOUNDED if there is a recursive function g : u — ► u
such that V/ G A, Vn, /(n) < g(n). A is a U°i class, if an only if A = P(T) for some
recursive tree T. We say that a tree T is HIGHLY RECURSIVE if T is a recursive,
finitely branching tree such that there is a recursive procedure which, given a =< a\,
...,a n > in T produces a canonical index of the set of immediate sucessors of a in
T, that is, produces a canonical index of {(3 =< <*i,..., a n , k > \fi GT}. Here we say
the canonical index, can(X) of the finite set X = {xi <...< x n ) C u is 2 Xl + ...+2 Xn
and the canonical index of the empty set is 0. We let D k denote the finite set whose
canonical index is k, that is can(D k ) = k. It is then the case that if A is a recursively
bounded n°! class, then A - P(T) for some highly recursive tree T. We note that
if T is a binary tree, then the set of paths through T is a collection of {0, 1} -valued
functions and by identifying each function / G P(T) with the set A f = {x\f(x) = 1}
of which / is the characteristic function, we can think of the set of paths through T
as a n°! class of sets.
We then have the following theorem:
Theorem 1.3.8 (MNR92a) Given a highly recursive nonmonotonic rule system
< U,N >, there is a highly recursive binary tree T such that there is an effective one-
to-one degree-preserving correspondence between the set of extensions of the system
and the set P(T) of infinite paths through T.
16
A bit more is required for the reverse implication, but it may be shown in the
following sense:
Theorem 1.3.9 (MNR92a) For any recursive binary tree, there is a highly re-
cursive nonmonotonic rule system such that there is an effective one-to-one degree-
preserving correspondence between the set of extensions of the system and the set
P{T) of infinite paths through T.
The significance of these results is that we can apply recursive IT ! classes to
obtain numerous corollaries [MNR92a, CR98].
Corollary 1.3.10 (CR99) Let S = (U,N) be a highly recursive nonmonotonic rule
system such that £(S) ^ 0. Then
(i) If S has only finitely many extensions, then every extension E of S is recursive.
A new representation result is given in chapter four for locally determined
nonmonotonic rule systems.
1.4 Common Derivations and Locally Determined Systems
In the second chapter we consider the finite case in which a nonmonotonic rule
system has a finite language and/or finitely many extensions. Within this chapter
we consider various forms of the common derivation of a sentence appearing in all or
some of the extensions of a nonmonotonic rule system. Certain forms of the common
derivation are explored not only in the classical sense but also using a constructive
view.
The infinite case is explored in the third chapter in which we have an infinite
number of extensions and/or an infinite language. Within this chapter, as in the
second, we consider various forms of the common derivation for a sentence appearing
in all or some of the extensions of a nonmonotonic rule system. Each of these is
17
explored in the classical sense as well as with a constructive view. We consider the
problem of characterizing the set of extensions of a locally finite nonmonotonic rule
system.
Locally determined nonmonotonic rule systems are introduced in the fourth
chapter. When considering nonmonotonic rule systems with an infinite language, a
problem arises in being able to determine at what stage we are sure to either have
concluded <j> or (in the case of restraints) not have concluded 4> for some 4> E U.
To solve this problem, the notion of "levels" was devised. Intuitively, we require
that for each i (as we take U to be enumerated {fa, fa, •••}), there is a fixed n x such
that the inclusion or exclusion of fa is determined by the n^-th stage. Hence the
term "locally determined" is used. This concept allows us to extend results from the
infinite case. The set of extensions of a locally determined nonmonotonic rule system
is characterized in general and in the effective setting.
In the fifth chapter, we consider the complexity of the sets of extensions and
explore the comparative complexity of the common derivations themselves. Within
these systems we explore both the finite and infinite settings, with the classical and
constructive views.
Alternate formalisms of nonmonotonic logic, specifically Default Logic and
Logic Programming, are discussed in the sixth chapter. We show the equivalence of
these formalisms to nonmonotonic rule systems and view some of the results of the
previous chapters in terms of these.
Lastly, in the seventh chapter we consider possible applications of the results
and future directions of the research.
CHAPTER 2
THE FINITE CASE
In this chapter we consider only those nonmonotonic rule systems which have
at least one but only finitely many extensions and/or a finite language. We consider
nonmonotonic rule systems in the classical view and also in the constructive view.
The underlying logic for a nonmonotonic rule system U =<U,N > can be any
form of logic desired. We will often take U to be the set of sentences of some propo-
sitional language. The usual monotonic rules of propositional logic are implicitly
included in each nonmonotonic rule system unless otherwise stated. We will choose
only one representative for each sentence in some systematic way so that there are
not infinitely many representations for each sentence in U. For example, -« V ~^b is
identified with -i(a A b).
2.1 Finite Classical Nonmonotonic Rule Systems
We consider a single nonmonotonic rule system U that has a finite number
of extensions and/or a finite language. We intend to explore the following question:
If <j) is a formula of the language L, such that <j> 6 S for every extension S of U,
then what, if anything, can be said about the theory and/or the formula and its
derivation in each extension. We would like to find a single rule that generates in
every extension. It would be most useful if the rule could tell us, through premises
and restraints, exactly what is required to derive 4> in the system. This rule need not
be in the set N of nonmonotonic rules, but it would be desirable to retain the same
set of extensions upon adding this rule into N.
18
19
We might first consider the simplest possible form of the common derivation,
namely taking <j> as an axiom : /(f). This will certainly generate <j> in every extension,
but we may gain new extensions when the rule is added to the set N of rules.
Example 2.1.7 Let U =< U,N > be the nonmonotonic rule system where U =
{a, b, c} and
N = {: {a, c}/b; : {b, c}/a; aVb: {a, b}/c}.
This system has two extensions Si = {a}, and S 2 = {b}. The sentence a V b appears
in each extension. The axiomatic common derivation for aV b will be : /0V6. Adding
this rule to the set N of rules will produce a third extension S 3 = {a V b, c}.
This formulation does not accomplish the purpose of the common derivation
in that it tells us nothing about what premises and restraints are involved in deriving
<j> in the various extensions of the original system. Thus, we consider other forms.
Definition 2.1.11 Let U =< U,N > be a finite nonmonotonic rule system. Then
U has finitely many extensions, S\, ..., S m . Suppose that G U appears in every Si.
Define the support-based common derivation d^ for (j) in U by
^=:{AA...A/? m |A£S t }/0.
Example 2.1.8 Letting U be the nonmonotonic rule system where U — {a,b} and
N = {: ^b/b; : &/-*; : /a}
we will have two extensions, Si = {a, b} and S 2 = {a, ->&}. The intersection of these
is {a} . Thus there are eight sentences not in Si and eight sentences not in S 2 ■ Hence
there are 64 sentences of the form fa A fa, where Pi £ Si and (3 2 $ S 2 . Some of
20
these will be trivially false, such as ->b A b. Some others will contain that which is
in neither extension such as -ia A ->a which will collapse to just ->a. The rest will
be restraints of a"*'. We see how the support-based common derivation becomes very
large very quickly. This will be a disadvantage.
We nevertheless get the following result:
Theorem 2.1.12 Let U =< U,N > be a finite nonmonotonic rule system. ThenU
has finitely many extensions. Suppose a sentence 4> £ U appears in every extension
of the system. Let d^ be the common derivation of <f> as defined in Definition 2.1.11.
Then, d^ applies in every extension of the system U and
£(U) = £(<U,Nu{d*} >).
Proof: Let U =< U, N > be a nonmonotonic rule system with finitely many
extensions Si , ..., S m . Suppose a sentence <f> e U appears in every extension of
the system. Let rf* be the common derivation of (j) as defined in Definition 2.1.11.
Consider an arbitrary extension Sj oiU. Take any conjunction &A...A/8U such that
(3{ $ S t . Then fy <£ Sj so that the conjunction (3 x r\.../\f5 m is not in Sj and thus none
of the restraints of d* is in Sj. Thus d? applies in Sj and therefore it applies in every
extension of the system U. We now have that
£(U)CS{<U,Nu{dfi} >).
To show that we retain the same set of extensions, suppose that S is an extension
of < U, N U {d*} > that is not an extension of U. Then S is not S t for any
i e {l,2,...,m}. Since S is not an extension of U the new rule must apply in S .
The set of extensions of U is noninclusive so that there exist ip x , ..., tjj m e S such
that tpi £ Si. Since we have implicitly included the rules of propositional logic, we
have that xpiA...AijJ m eS . By the definition of d 4 ", this conjunction is a restraint of
21
d?. Thus the rule d? does not apply in So contradicting that So is a new extension.
Thus,
€{U) = £{<U,NU {&}>).
Similarly, we might construct a rule consisting only of premises and a conclu-
sion. The advantage of this form of the common derivation is that it reveals, at least
in part, what is involved in deriving <fi in the extensions. The disadvantage is that
we must first know the extensions of the system before we can construct the rule.
Finding this rule takes considerably more time than would a rule which relied only
on the system U without having to find the extensions. Also, this rule would not
be possible in the infinite case. Thus we seek a form of the common derivation that
would be based on the rules of the system itself, not the extensions, and would also
be possible in the infinite case. We find the following form. For a sequence of sets
A\, . . . , A m of sets of formulas, let f\ t A x denote the set of conjunctions a x A . . . A a m
where each a t e A x . Let A{A t denote the usual conjunction where the formulas of
Ai are themselves conjuncted to form formulas. The notations \J \ Ai and VjA; are
similarly defined.
Definition 2.1.13 Letting U be a nonmonotonic rule system with a finite language
L, we will have a finite number of extensions. List the extensions as {Si, . . . , S m }.
Let pi be the proof scheme deriving (j) in the extension Sj and consider the last rule,
fj in each Pi. Define the standard common derivation to be d/ be the nonmonotonic
rule
i
We will henceforth refer to the nonmonotonic rule system, < U, A r U{d (/) 1 } >, asU + .
22
Theorem 2.1.14 Let U =< U,N > be a nonmonotonic rule system with a finite
language L. Then, for every sentence <fi S (~)£(U), there exists a standard common
derivation d^ x that generates <j) in every extension ofU.
Proof: List the extensions of U as {S\, . . . , S m }. Suppose that <fi is a sentence
oft/ that appears in every extension of the system. Since <j> appears in every extension
of the system, there must be a proof scheme pi for each S{ deriving <f> in that extension.
List the proof schemes for 4> as {pi, ..., p m }. Consider the last rule, r { = P(r t ) : fa 1 ,
..., /3 tt l /<f) of each proof scheme Pi. Let d^ 1 be the nonmonotonic rule
V i P(r t ):/\R(r i )/+.
i
Let Si be any extension of U. We only have to show that d/ applies in $. Since Si
is an extension of U, we have that the last rule r% of the proof scheme Pi applies in
St. Thus, P( ri ) 6 St and ft', ..., fa* $ Si. Therefore,
P(n) = y l P{r l ) e s t .
For any 8 x /\...t\5 m € Ai^(n), <5» = P\ for some t, so S t £ S ( and by the standard
propositional logic, d/ applies in Si and concludes c(d/) = <j>.
The common derivation of any formula <f> in U may not be found in N as
illustrated by the nonmonotonic rule system of Example 1.3.3. Recall that
N = {:{a}/b,:{c}/b,:{a}/c,:{c}/a},
and that U has the two extensions S\ = {b, c) and S 2 = {b, a}. Also, as before,
GD(N,S 1 ) = {:{a}/b,:{a}/c}
and
GD(N,S 2 ) = {:{c}/b,:{c}/a}.
23
There is no rule of N that derives b in both extensions. However, we may consider
the common derivation of b in U which is
d\ =: {(a A c)}/b V 6 =: {(a A c)}/b.
Then, rf 1 ^ will generate b in each of these extensions. To see this, note that d x b has
no premises, and a A c £ S since in S\ we have that a £ S\ since : {a)/b applies in
S\. In St, c £ S 2 since : {a}/b applies.
Let U —< U, N > be an nonmonotonic rule system with a sentence 4> occuring
in every extension of the system. Let d/ be the common derivation as defined in
Definition 2.1.13. We find that the sets of extensions of the original system U and
the set of extensions of the new system U+ will, under sufficient conditions, be the
same. However, U + may have an extra extension, while still having as extensions all
the extensions of U.
Theorem 2.1.15 Let U =< U,N > be a nonmonotonic rule system with a finite
language L such that a sentence <j) e U appears in every extension of the system. Let
d^ be the common derivation of (j) as in Definition 2.1.13. Then,
E{U) C £{U + ).
Proof: Let U =< U, N > be a nonmonotonic rule system with a finite lan-
guage L and suppose that a sentence <j> € U appears in every extension of the system.
Let dj, be the standard common derivation of (j) as in Definition 2.1.13. Let S be any
extension of U. Then, to show that S is an extension of U + , we need to show that
for any u G U, u G S if and only if there is a proof scheme p for u in the new system
such that all premises in p are in S and all restraints in p are outside of S. Suppose
first that u e S. Since 5 is an extension of the system U, there is a proof scheme p
for u such that all premises in p are in S and all restraints in p are outside of 5.
24
It is clear that p is still a proof scheme for u in the new system U + . Next suppose
that p is an 5-applicable proof scheme in U + . It suffices to consider the last rule r of
the proof scheme p where the premises of r are in S, the restraints of r are not in S,
and the conclusion of r is u. If r is the common derivation then u = <f> so the <fi e S
by the hypothesis. Thus, S is an extension of U + . Hence,
£(U)C£(<U,NU{d^ 1 } >).
We can generalize this result in the following way.
Theorem 2.1.16 Let U =< U,N > be a nonmonotonic rule system with a finite
language L such that a sentence 4> G U appears in every extension of the system. Let
r^ be any nonmonotonic rule concluding <f> such that r^ applies in every extension of
U. Then,
£(U)C£{<U,Nu{ r<j> }>).
Proof: The proof of this theorem mimics that of the previous theorem. The
key part of the proof showing that an extension S of U is closed under the expanded
system U + follows as above since the conclusion 4> of the new rule r^ is assumed to
be in every extension of U.
We see that the sets of extensions may or may not be equal in that the new
system U + may or may not have one or more extra extensions. Recall Example 1.3.3.
Consider the nonmonotonic rule system U where U = {a,b, c}, N = {: a/b, :
c/b, : a/c, : c/a}, and U has the two extensions S\ = {b, c} and 52 = {b, a}, and the
common derivation of b in U is d x h =:oA c/b. Adding this new rule to N, we see
that < U, N U {d l b } > has the same extensions 5 X and 5 2 , since applying d x b does
25
not prevent the application of any rule in N or allow the application of any rules in
the system that were not previously applied.
To be precise, suppose there was a new extension S different from S\ and
52- Then, the new rule d 1 ^ must be generating for S. This implies that b € S and
(a Ac) £ S. It follows that either a £ S or c <£ S. Thus, one of the original rules,
either : {a}/b or : {c}/b, will generate for S and either : {a}/c or : {c}/a will also
generate for 5. Then, either c e S or a e S, but this means that either Si C S or
S 2 C S. By the noninclusive property, either S = Si or S = S 2 .
Example 2.1.9 Now consider the nonmonotonic rule system U where
U = {Pi,P2,Ci,c 2 ,a}
and
N = {pi\ /ci;p2 : /w- a,pi/p2',: a,p2/pi;: pufr/pi Vp 2 ;ci V c 2 : c u c 2 /a}.
This theory has two extensions,
Si = {P2,C 2 },
and
S 2 = {pi,ci}.
The formula c\ V c 2 is in each extension and we find that
r\=Pi'. /c 2 ,
and
so that
r 2 =Pi- /ci,
^civcz =Pi Vp 2 : /ci Vc 2 .
26
Then, S x and S 2 are both extensions of < U, NU {d} ClVC2 } >, but this new nonmono-
tonic rule system will have a third extension
S = (pj Vp 2 ,ciVc 2l o},
which is not an extension of the original system U.
In the previous example, 5 3 is the only new extension obtained by adding the
common derivation to the set of rules. To see this, let S be any new extension. The
common derivation must generate for S, else S is an extension of the original system.
Thus, we have that p x Vp 2 E S so that the conclusion c x \Zc 2 is in 5 as well. If p Y e S,
then c x E S by the rule p x : fc\ so that S\ C S, a contradiction to the noninclusive
property of extensions, since S is not an extension of the original system. Similarly,
if p 2 E S, then c 2 E S so that S 2 C S, a contradiction. Thus, neither of p x or p 2 is
in S. Also, if a is not in S, then the rule : {a,p 2 }/p x applies to conclude p x in S.
Thus, a E S. From this we now have that 5 3 C S so that 5 3 = S since extensions
are noninclusive. Thus, there is only the one new extension.
Since the standard common derivation is based on the rules in the proof scheme
of (j) instead of the extensions of the system, it might be possible in an infinite system.
The good news is that the set of extensions of the new system contains the set of
extensions of the original system. The bad news is that these sets of extensions may
not be equal. We would prefer that they be equal.
We see that this form of the common derivation does not reach the goals that
we were after, although interesting. We strive further towards the goal of equal sets
of extensions in the next chapter.
If we have a formula appearing in some but not all the extensions of U, we
may in the same fashion as Definition 2.1.13 create a common derivation for that
generates <j> in each extension of U in which it appears. However, we find that in this
case Theorem 2.1.15 becomes false, as the next example illustrates.
27
Example 2.1.10 Let U =< U,N > be the nonmonotonic rule system where
N = {: {ai,a 2 }/a 3 ,: {a 2 ,a 3 }/a x ,: {a 1 ,a 3 }/a 2 ,
Pi : { _, ai}/ci,P2 : {^a 2 }/c 2 ,a 3 : jp x Vp 2 ,a x : M,a 2 : /p 2 }.
77iis theory has as three of its extensions,
Si = Cn({a 3 ,pi Vp 2 }),
5 2 = Cn({a 2 ,p 2 ,c 2 }),
and
5 3 = Cn({a x ,p x ,c x }).
We see £/ia£ i/ie formula c x V C2 is in both S 2 and S3, but is not in S\. We find the
standard common derivation for c x V c 2 to be
d\ x \, C2 =P\ Vp 2 : {-1(01 V a 2 )}/c l V c 2 .
Adding this new rule to the set of rules N , we find that both S 2 and S3 are extensions
of the new nonmonotonic rule system < U, NU {d} Cl \/ C2 } >. Si, however, is not an
extension of < U, N U {d 1 Cl vc 2 } > since it it no longer closed under the set of rules.
It is important to note that S\ is a subset of {a 3 ,p x Vp 2 , C\ Vc 2 } which is an extension
of<U,NU{d l ClVCi } >.
Theorem 2.1.17 Let U =< U,N > be a nonmonotonic rule system with a finite
language L such that 4> appears in some but not all of the extensions and each gener-
ating rule for each extension S is a generating rule for SL){(f>}. Consider d}^ to be the
common derivation of(f> as defined in Definition 2.1.13. Then, for any extension S of
U, such that <j> € 5 there is an extension S + ofU + such that S = S + . Furthermore,
any extension oflA + which is not an extension ofll must contain <j>.
28
Proof: Suppose that U is a nonmonotonic rule system with a finite language
L such that (f> appears in at least one, but not all of the extensions. Consider d 1 ^ to
be the standard common derivation of <f> as defined in Theorem 2.1.13. If 4> appears
in only one of the extensions of U, then the common derivation d 1 ^ is found in N
so that < U,N >= U + , and the theorem is trivially true. Thus, suppose that $
appears in at least two extensions of the nonmonotonic rule system U, but does not
appear in every extension. Let $ be an extension of U. If $ is an extension of the
new system U + , we are done. Also, if is in $, then $ is clearly an extension of
< U, N U {d 1 ^} > as in the proof of Theorem 2.1.15. Hence, consider the case in
which S is an extension of the new system U + , but is not an extension of the old
system U. If d 1 ^ does not generate for S, then
S = GD{N U {d\}, S) = GD(N, S)
so that S is an extension of the system U, a contradiction. Thus, d 1 ^ generates for
Si so that
<P = c(d\) e c(GD(N U {d\}, S)) = S.
The added conditions of this theorem that require each generating rule for
each extension S to be a generating rule for S U {$} are necessary for the following
reason. If we consider the previous example, and add the rule a 3 : /-.(ci V c 2 ) to the
set ./V of rules, S\ becomes
S\ = {a 3 ,pi Vpa,-i(ei Vc 2 )}.
Then, ci V c 2 cannot be added to Si.
Now we explore the question of what happens if we take the process further;
finding the intersection of the extensions, creating a common derivation, and then
adding that rule to the nonmonotonic rule system, over and over.
29
Suppose we let Ii be the intersection of all the extensions of the original
nonmonotonic rule system U. Then, in Example 2.1.9
h =Cn({(p 2 Ac 2 )V(p 1 Ac 1 )}).
We consider the new rule system
U 2 =< U,N 3 >=< U,Nu{d\ x v C2 } >
and the set I 2 of all conclusions common to every extension of U 2 . We find that
h = Cn({( Pl Vp 2 ) A (c, Vc 2 )}) C h.
Moreover, we could choose a conclusion common to all the extensions of U 2 ,
such as pi Vp 2 . This has the common derivation
rf 2 Pl v P2 =: {oVpi,oVp2,o,pi Vp 2 }M Vp 2 -
In any new extension S of
U3=<U,N 2 U{d 2 PlVp2 } >
that was not an extension of the theory U 2 , this common derivation must apply. Sim-
ilarly to the previous argument, none of pi,p 2 , ci or c 2 can be in S else we contradict
the noninclusive property of extensions. p x V p 2 must be in S since the common
derivation applies. Thus, by the common derivation for c x Vc 2 , we conclude c x V c 2 in
S and thus a is in S by the appropriate rule from N. This is a contradiction since the
common derivation requires that a not be in S. Thus, there are no new extensions,
that is, U 2 has the same set of extensions as U3.
On a different note, we may force the intersections I x and I 2 to be equal by
taking <f>tobef\Ii. This appears in every extension of U. Letting
Ni = Nu{d l +},
30
we find that if S is any new extension, then € S since the common derivation must
apply (else S is not new). We then get the following theorem.
Theorem 2.1.18 Let <f> be the conjunction of the intersection I x of all extensions of
U. Then the intersection I 2 of all extensions ofU + equals Iy.
Proof: Clearly we have that I 2 C I x . Now suppose that ip € /j and let S
be any extension of U + . If S is an extension of U then tp G S since xjj e I\. Thus,
suppose that 5 is an extension of U + that is not an extension of the original system
U. This new extension must contain </>. Since <fi is the conjunction of the intersection
of extensions I\, we have that <j) — > ip. Thus the extension S must contain i/j. Thus,
1% = h-
We may consider any nonmonotonic rule system U, and the set
h = f]e{U).
For every <fi in this set, we can find a common derivation d x $ which generates in
each extension S of U. Consider the nonmonotonic rule system U 2 defined by
<U,Nu{d l t\<fieh}>.
We may then repeat the procedure to find
I 2 = f)£(U 2 ),
and if this set is not empty, then we can find common derivations d 2 ^ for any <j> in
I 2 such that d 2 ^ generates <j> in every extension S of U 2 . Then, we may consider the
nonmonotonic rule system Ui defined by
<U,N 2 U{d\\(t>^I 2 }> .
We continue this construction by, assuming that U n is defined, let
I n = S{U n ).
31
Then, letting d% be the common derivation for <f> £ I n in U n , we define U n+ y to be
<^iV n U{(T^ €/„}>.
This may be continued until I k is empty for some k and/or N k = Ni for all I > k
for some k. This inductive definition begs the following questions. Is there a limit to
this process, i.e., is there always some k for which I k is empty and/or JV fc = N t for
all / > A;? Does it make a difference if we work in the case where N is finite versus
countably or uncountably infinite? These questions should be investigated.
Example 2.1.11 Consider the nonmonotonic rule system of Example 1.3.3. Using
this nonmonotonic rule system, we would find N 2 to be
N U {d\} = {: {a}/b, : {c}/b, : {a}/c, : {c}/a, : {(a A c)}/b).
U2 has the same extensions as U so that I 2 = h = {b} and d 2 b = d l b- Then N k = N 2
for all k > 1 .
Remark 2.1.19 By Theorem 2.1.15, we have that E(U) C S(U 2 ) C ... C £{U n ) C
£(Un+i) C ....
For a finite language, or just a finite 7 1; we must eventually have 7 n+1 = /„
for some n. At this point, we find that we will have a common derivation in N n for
each <j> G /„, when we consider N n to be defined using all of the common derivations
for conclusions in /„_!. U n will be said to HAVE common derivations.
Theorem 2.1.20 For any nonmonotonic rule system U with finite I\ or with finite
N, there exists an n such that U n has common derivations, and li n is equivalent to
the nonmonotonic rule system U n+ k for any k.
32
For an alternate approach, we might consider the nonmonotonic rule system
U and the set I\ as before. However, we may choose one element cf> from I x and define
< U,N 2 > to be the nonmonotonic rule system
U +
as seen for Example 6.3.26. We may then consider the set of all formulas which
appear in every extension of < U,N 2 >, choose some V among those, and define
<U,N 3 > to be
<u,N 2 u{d\}> .
We may continue in this way with the same result as in Theorem 2.1.20.
2.2 Finite Constructive Nonmonotonic Rule Systems
Again, consider a single nonmonotonic rule system U with a finite set of ex-
tensions and/or a finite language. In this section, we consider the same question
about nonmonotonic rule systems as in the previous section, but use a constructive
approach. That is, we consider that pVq is not derived unless one of p or q is derived.
Note that we will no longer implicitly assume the propositional axiom pV->p. Had we
chosen to keep this axiom, while considering a constructive view, all the extensions of
every system would be complete, and consequently uninteresting. We will, however,
keep the propositional rules for conjunctions as we did in the classical case.
Again, we consider 0, a formula of the language L such that <j> e (~)£{U).
Then ^ G 5 for every extension S of U. Since each extension S is of the form
c(GD(N, S)), there must be, as before, a proof scheme pi deriving for each extension
St. The advantage of the constructive approach is that it allows us to view each set
of restraints as a single formula instead of as a set of formulas. Then, instead of
asking if each element of the set of restraints is not in a context, we would ask if the
restraint itself is not in the context. As it stands, the last rule r t in each proof scheme
33
Pi has as its restraints the set {(3\, ...,#**} for some /?v formulas of the language. We
may instead let R(n) = /3\V ... Vf3\. Then flfa) is in the extension S t if and only
if |9j e Si for some j, a contradiction since r, generates for Sf. We find that several
of the theorems of the last section still hold.
Theorem 2.2.21 For any formula <f> of the finite language L such that (j) 6 f\£{U),
4> has a common derivation d 1 ^ which generates (/> in each extension S ofU where U
is a constructive nonmonotonic rule system.
Proof : Suppose U is a constructive nonmonotonic rule system with a finite
language L. Suppose further that <f> is a sentence of U that appears in every extension
of the system. List the extensions of U as Si, . . . , S m . Then for each extension 5 8 of
U there is a proof scheme p t deriving in S t . Consider the last rule, r t = P(n) : ft*,
..., 0ti % /4 of each proof scheme p { . Let d/ be the nonmonotonic rule
^P^-.^RirJ/cf).
i
Let Si be any extension of U. We only have left to show that d/ applies in St. Since
Si is an extension of U, we have that there is some proof scheme p { that derives in
S^ Since this proof scheme derives in $, each rule in the proof scheme applies in
S t so that r t applies in Si. Thus, P(r t ) e S z and ft*", ..., ft.' <£ S { . Thus,
P(n) = ViP(n) e s t
and any ^A...A(5 m 6 A* Rfc) will not be in S t . Thus, d/ applies in 5, and concludes
c(d/) = <^>. Thus, for any formula 4> of the language such that G f|£(^), </> has a
common derivation d 1 ^ which generates <\> in each extension S of W. Note that d\
may be in TV, but then U + will have the same set of extensions as U.
34
Example 2.2.12 Consider the nonmonotonic rule system of Example 1.3.3. Under
the approach of this section, we let
N = {: a/b, : c/b, : a/c, : c/a}.
Then the nonmonotonic rule system U has the two extensions
Sr = {b )C }
and
S 2 = {b,a}.
Also,
GD{N,S l ) = {:a/b,:a/c}
and
GD(N,S 2 ) = {:c/b,:c/a}.
Just as before, there is no rule of N that derives b in both extensions. However, we
may condsider the common derivation ofbinU by the methods of this section, which
is
d\ -. (oAc)/6.
Then, d l b will generate b in each of these extensions. Compare this version of the
common derivation of b in U to that of the previous section where we had
d\=:{(aAc)}/b.
We see that the two methods produce very similar results, but that the common deriva-
tion produced by the methods of this section is computationally simpler.
By the same arguement as in Theorem 2.1.15, we still have that
S{U)CS{<U,Nu{d\}>)
35
for any e f\S(U). Equivalently, £{U) C £(< U, NU {d^} >), for any € f)£(U).
Also as before, the converse of this theorem is false, as illustrated in example 2.1.9.
We must then ask if there might be a better formulation of the common
derivation that would ensure that same set of extensions when added to the system.
There is, but it is not without strings attached.
Theorem 2.2.22 For any formula $ of a finite language such that € f)S(U),
define the strong common derivation d*^ to be
V,P(r<) :|J J2(r«)M
i
Then, rf% e GD(N U {d* <t> },C]£(U)).
Proof : Let be a formula of the language such that e f]£{U). Consider
<J% as defined above. Clearly d% £ N U {d*^}. Now, for every extension $ in £{U)
we have that some proof scheme p t generates in S t so that P{ri) G S t . Thus,
P{d\) = V l P(r l ) e f\£(U). Lastly, we have that /*(<*%) = (J^,-) C f)£(U) if
and only if Rfa) C f|£(W) for all ». However, this is if and only if R(n) C 5 2 for
some extension $ where Pi generates for 5,-. Then, flfo) 6 5,, a contradiction. So
we have that R{d* (j) ) is not a subset off\£(U). Thus d% generates <f> in f|£(W).
Note that although this new rule generates for the intersection of all the ex-
tensions, it may not generate for each particular extension.
Example 2.2.13 Consider the nonmonotonic rule system U where
N = {:{a}/b,:{b}/a}.
This rule theory has two extensions,
Si = {b},
36
and
S 2 = {a}.
We have that the formula a V b is in both of the extensions and we find that
d* a vb ='■ {a, b}/a V b.
By the theorem, d* aVb generates for the intersection of the two extensions. However,
it does not generate for either of the extensions Si or S 2 since b € S\ and a e S 2 ,
respectively.
We may again inductively define the nonmonotonic rule system U n as we did in
the last section. Investigations into the questions raised by this definition are further
warrented in this setting as the common derivations are computationally simpler and
the constructive view may make the difference in what the answer to those questions
will be.
Example 2.2.14 Consider the nonmonotonic rule system of Example 1.3.3. Using
this rule system, and the methods of this section, we would find N 2 to be
N U {d\} = {: a/b, : c/b, : a/c, : c/a, : (a A c)/b).
Again, U 2 has the same extensions as U so that I 2 = h = {b} and d 2 b = d\. Then
N k = N 2 for allk > 1.
2.3 Characterizing the Set of Extensions
Now, since the intersections of families of extensions are of particular interest,
we might ask which families of extensions have intersections which yield a specific
theory. Knowing this, given a theory which we desire to see as the intersection of
extensions we may create the nonmonotonic rule system whose extensions intersect to
yield that theory. Note that we will not implicitly assume any rules of propositional
logic for the case of this construction.
37
Theorem 2.3.23 Given any finite family of sets
F = {Ti,T 2 , . . .,T n },
in the language L there is a nonmonotonic rule system U whose set of extensions
£{U) is exactly F.
Proof: Let
F = {T X ,T 2 , . . . ,T n },
be any finite family of sets. We create the system U in the following way. Let U be
the set of atoms of the language L. Let
N = {:{A j T j \j^i}/AT i \l<i<n}.
Then, U will have F as its set of extensions.
For example, for the family {{a, b, c}, {a, c, d}, {a, b, d}} we would choose the
nonmonotonic rule system < U, N > where
N = {: {aAbAc,aAc/\d}/aAbAd;: {aAbAc,aAbAd}/aAcAd;: {aAbAd,aAcAd}/aAbAc.
This system will have exactly the three extensions: {a, b, c}, {a, c, d}, and {a, b, d}.
So we see that any given theory may be derived as the intersection of a set of
extensions by determining what family of sets intersects to yield the desired theory,
and then constructing the appropriate nonmonotonic rule system whose extensions
are that family.
The constructive case will be different only in that the number of possible
extensions that are acceptable is greatly reduced. This is explored in detail in terms
of Default Logic in Chapter 6.
CHAPTER 3
THE INFINITE CASE
In this chapter we consider nonmonotonic rule systems with infinitely many
extensions and an infinite language. This necessitates the concept of a locally finite
system as seen in the introduction. We first consider nonmonotonic rule systems in
the classical view and then in the constructive view. Lastly, we consider the task of
characterizing the set of extensions of a locally finite nonmonotonic rule system.
3.1 Locally Finite Classical Nonmonotonic Rule Systems
Considering locally finite nonmonotonic rule systems, we can have results for
the infinite case similar to those of the finite case. We should note, however, that the
support-based common derivation d? as shown in the finite case is no longer possible
in the infinite case since it would result in an infinite conjunction in the restraints of
the rule. Still applicable, however, is the standard common derivation d 1 ^.
Theorem 3.1.24 Let U =< U,N > be a locally finite nonmonotonic rule system.
Then, for every sentence <j> € f\€(U), there exists a standard common derivation d/
that generates 4> in every extension ofU.
Proof: Suppose U is a locally finite nonmonotonic rule system. Suppose
further that $ is a sentence of U that appears in every extension of the system. Since
the system is locally finite, we have that there are only finitely many minimal proof
schemes for <f>. List the proof schemes for (j) as Dr+ = {p u ..., p m }. Consider the
last rule, r { = P(n) : fa 1 , ..., fa*l<$> of each proof scheme ft. Now, since <j) appears
in every extension of the system, we have that for each extension S, there is a proof
38
39
scheme that derives 4> in S, call it ps. Since each rule of the proof scheme applies in
S, we know that there must be a minimal proof scheme p i: for some i 6 {1, ..., m},
contained in p s that derives <j> in S. Let d/ be the nonmonotonic rule
i
Let S be any extension of U. We only have left to show that d^ 1 applies in 5. Since
S is an extension of U, we have that there is some minimal proof scheme p l e Dr^
that derives (j> in S. Since this proof scheme derives </> in S, each rule in the proof
scheme applies in S so that r { applies in S. Thus, -P(rj) € 5 and /V, ■••, /V ^ 5.
Thus,
P(r>) = s/iPin) e s
and any 5iA...A5 m € Ai R( r i) w ^ not De in S. Thus, d$ applies in S and concludes
cid^) = $.
We must ask several questions concerning how this new rule effects the system
U. First, if the system U is locally finite, then what happens when we add in the
new rule to consider the system U + . Is it still locally finite? In terms of the sets of
extensions, will we find that
£{U) = E{U + )1
We find that the expanded system may no longer be locally finite, as seen in
the following example.
Example 3.1.15 Let U —< U,N > be the nonmonotonic rule system where
U = {ai, a 2 , b, d, e] U {ci\i € lj}
and
N = {ai : /b;a 2 : /&; : a u d/a 2 ;: a 2 ,d/ai;: ai,a 2 /ai Vo 2 ;ai V a 2 ,b: ai,a 2 /d}
40
U{ai V a 2 , b : Oi, a 2 /cj|i G a;}
U{cj : Oi,a 2 /e|2 G a;}.
This system has two extensions, Si = {ai,b}, and S 2 = {a 2 ,6}. The atom b appears
in each and has the standard common derivation d 1 ^ = a\ V a 2 : jb. Upon adding this
rule to the set N, we find that the new system provides an infinite number of minimal
proof schemes for e. Thus the new system is not locally finite.
The problem arises that there may be infinitely many distinct rules concluding
a sentence ip G U that are not applied in any extensions and therefore do not enter
into the set of minimal proof schemes for tp. However, the addition of the common
derivation to the set of nonmonotonic rules may allow these rules to be applicable
and thereby the set of minimal proof schemes to be infinite. Then the new system
is not locally finite. To mend this problem, we must rid the system of rules that are
not applied in any extension prior to the addition of the common derivation.
Definition 3.1.25 Call a nonmnotonic rule r G N ACTIVE if it applies in some
extension of the rule system U; call the rule DORMANT, if it does not apply in any
extension of the system. Call a nonmonotonic rule system U DORMANT if every
rule in N is dormant. Call the system PARTIALLY DORMANT if N has at least
one dormant rule and at least one active rule. Finally, call the system ACTIVE if
every rule in N is active.
[Note that if a system is dormant, then it has no extensions.]
Theorem 3.1.26 Let U =< U,N > be a locally finite active nonomonotonic rule
system such that </> appears in every extension of the system. If d/ is the standard
common derivation for <f> in U, then U + is locally finite and active.
Proof: Suppose U is a locally finite active nonomonotonic rule system such
that <f> appears in every extension of the system. Let d/ be the standard common
41
derivation for </> in U. Consider the nonmonotonic rule system, U + created by adding
the common derivation to the set of nonmonotonic rules:
Given that the original system is active, we have that every rule in N applies in some
extension of U. Since the system < U, N U {d/} > will have the same extensions
as the original system, and any extra extensions obtained are such that the common
derivation applies, we have that the new system is active. Further, U is locally finite
so that the set of minimal proof schemes for any sentence ip 6 U is finite. These sets
of minimal proof schemes will remain finite unless applying the common derivation
allows the application of an infinite list of rules that conclude some ip 6 U. Suppose
this is true. This infinite list of rules must be from N, as the common derivation is the
only rule added to obtain the new system. Thus, these rules are active so that each
rule is applied in some extension of U. Thus, each rule provides a proof scheme for
if) in U. Since each rule is distinct and concludes ip, we have that none of these proof
schemes is contained in any other so that there are infinitely many minimal proof
schemes for ijj and U is not locally finite, a contradiction. Thus, the new system, U +
is locally finite.
Let U =< U, N > be a nonmonotonic rule system with a sentence 4> occuring
in every extension of the system. Let d/ be the standard common derivation as
defined in Theorem 3.1.24. We find that the sets of extensions of the original system
U and the set of extensions of the new system U + will, under sufficient conditions,
be the same. However, U + may have an extra extension, while still retaining all the
extensions of U.
Theorem 3.1.27 Let U =< U,N > be a locally finite nonmonotonic rule system
such that a sentence (j) e U appears in every extension of the system. Let d 1 be the
42
standard common derivation of (j) as defined in Theorem 3.1.24. Then,
£{U) C E{U + ).
Proof: The proof for this theorem is similar to that of Theorem 2.1.15.
We can generalize this result in the following way, as in the finite chapter:
Theorem 3.1.28 Let U =< U,N > be a locally finite nonmonotonic rule system
such that a sentence (j) G U appears in every extension of the system. Let r^ be any
nonmonotonic rule concluding <j> such that r^ applies in every extension ofU. Then,
£(U)C£(<U,Nu{r+}>).
Proof: The proof of this theorem mimics that of the previous theorem.
We see that the sets of extensions may or may not be equal in that the new
system U + may have one or more extra extensions. Consider the following example:
Example 3.1.16 Consider the nonmonotonic rule system U from Example 3.1.15.
This system has the two extensions S\ = {ai,b}, and S 2 = {a 2 ,b}. The atom b
appears in each and has terminal rules
r x = a\ : /b,
and
r 2 = a 2 : /b,
so that the standard common derivation is
d 1 t = Oi V a 2 : /b.
43
Upon adding this rule to the set N, we find that the new system aquires and extra
extension. S\ and S 2 are both extensions of < U, N U {d l b} >, but we will have a
third extension
S 3 = {ai V a 2 , b, d, e) U {q,\i E u},
which is not an extension of the original system U.
In the previous example, S3 is the only new extension obtained by adding the
common derivation to the set of rules. To see this, let 5 be any new extension. The
common derivation must generate for S, else S is an extension of the original system.
Thus, we have that a\ V a 2 € S so that the conclusion b is in S as well. If ai € S,
then b £ S by the rule ai : /b so that Si C 5, a contradiction to the noninclusive
property of extensions, since S is not an extension of the original system. Similarly,
if 02 G 5, then b € S so that 5 2 ^ S, a contradiction. Thus, neither of a^ or a 2 is in
S. Then the rules : ai,a 2 /a\ Va 2 and a^V a 2 : Oi, a 2 /cj for each t apply so that Cj 6 S
for each ». From this we now have that 53 C 5 so that S3 = S since extensions are
noninclusive. Thus, there is only the one new extension.
Further, we might try considering active nonmonotonic rule systems, in hopes
that this would cure the new system of its extra extensions. This does not help, as
seen in the next example.
Example 3.1.17 Consider the nonmonotonic rule system U where
U~ {PI,P2,JUJ2,C}
and
N = {pi : ^'i/c;p 2 : ^j 2 /c; : pi/p 2 ; : p 2 /p\\c : ^ji/^j 2 ; c : ->j 2 /^ii}-
This system can be taken to be active and has two extensions,
Si = {Pi,c,^ 2 },
44
and
S2 = {P2,C,^ji}.
c appears in both extensions and we see that
d X e = Pi V p 2 : -iji A -»J2/c.
Adding this rule to the set N, we find that the new system, < U, N U {d x c } >, has
both S\ and S 2 as extensions but also has two other extensions, S3 and S4 where
53 = {Pi,->ji,c},
and
54 = {p 2 ,-\?2,c}.
At this point, all possible versions of the common derivation that carry over
from the finite classical case have been exhausted. Yet we crave a form of the common
derivation that may have better luck retaining the same set of extensions when added
to the original set N of rules. We turn then to the following more complex rules.
These are constructed with more intricate restraints that are meant to rule out the
causes of extra extensions in U + .
Definition 3.1.29 We define two new versions of the common derivation, d]((p) and
d 2 ((j)) similarly to the definition of d/ in that we consider the last rule in each of the
minimal proof schemes of :
Suppose U is a locally finite nonmonotonic rule system. Suppose further that
is a sentence of U that appears in every extension of the system. Since the system
is locally finite, we have that there are only finitely many minimal proof schemes
for (j). List the proof schemes for <j> as Dr^ = {p u ..., p m }. Consider the last rule,
45
U = P{fi) : /?i\ ..., Pu/<l> of each proof scheme p { . Now, since (f> appears in every
extension of the system, we have that for each extension S, there is a proof scheme
that derives <j> in S, call it p s . Since each rule of the proof scheme applies in S\
we know that there must be a minimal proof scheme p t , for some I G {1, ..., m},
contained in p s , i.e. p { ■< p s , that derives 4> in S.
Define the refined common derivation di(4>) to be the nonmonotonic rule
V^) : /\ R(r t ) U \/(P(rO A [\/ flfc)])/*.
i i
Further, define the strong refined common derivation d 2 (<t>) to be the nonmonotonic
rule
^P(n) : /\ R(n) u /\(P( r< ) a [\/ R(n)])/4>.
Taking each rule in its turn, we find different properties. Since (j) belongs
to each extension of the system, it follows as usual that < U,N U {di ((f))} > and
< U, N U {d 2 {(f))} > each retain the extensions of < U, N >. Considering the rule
d\(4>) we obtain the following results:
Theorem 3.1.30 Let U =< U,N > be a locally finite active nonomonotonic rule
system such that (p appears in every extension of the system. If di((f)) is the refined
common derivation for in U, then < U, N U {d\((j))} > is locally finite and active.
Proof: Suppose U is a locally finite active nonomonotonic rule system such
that (j> appears in every extension of the system. Let d\{4>) be the refined common
derivation for <j> in U. Consider the nonmonotonic rule system created by adding the
refined common derivation to the set of nonmonotonic rules:
<U,Nu{d l {(t>)}> .
46
Given that the original system is active, we have that every rule in N applies in some
extension of U. Since the system < U, N U {di((f))} > will retain the extensions of
the original system, and any extra extensions obtained are such that the common
derivation applies, we have that the new system is active. Further, the system U is
locally finite so that the set of minimal proof schemes for any sentence ip G U is finite.
These sets of minimal proof schemes will remain finite unless applying the common
derivation allows the application of an infinite list of rules that conclude some ip G U.
Suppose this is true. This infinite list of rules must be from N, as the common
derivation is the only rule added to obtain the new system. Thus, these rules are
active so that each rule is applied in some extension of U. Thus, each rule provides
a proof scheme for tp in U. Since each rule is distinct and concludes ip, we have that
none of these proof schemes is contained in any other so that there are infinitely
many minimal proof schemes for ip and li is not locally finite, a contradiction. Thus,
the new system, <U,Nl) {di(4>)} > is locally finite.
However, using this version of the common derivation, we may not have that
di(4>) applies in every extension of the system. The reason for this is that the dis-
junction in the restraints,
Y^fojAlVflfo)]),
cannot be found in any extension of the system. For this to be true, none of the
(P(r<) A (V *(*)])
may appear in any extension of the system. This is too much to ask, as we can only
be certain that for each extension there is at least one rule r* that applies. There
may be one or more rules that do not apply; i.e. there may be a rule r, that does
not apply such that P(tj) is in the extension, but some restraint of r, is also in the
extension. In that case, P(rj) A [V R(ri)]) is in the extension so that the disjunction
V(^)A[\/«(n)])
47
is in the exension and the common derivation d\ (<j>) does not apply.
Considering the strong refined common derivation, d 2 (<f>), we get just the
opposite problem. We find that this version of the common derivation applies in
every extension of the system, but may create new extensions when added to the set
of nonmonotonic rules.
Theorem 3.1.31 Let U =< U,N > be a locally finite nonmonotonic rule system
such that a sentence $EU appears in every extension of the system. Let d 2 (<f>) be the
strong refined common derivation of <j> as defined in Definition 3.1.29. Then, d 2 (</>)
applies in every extension of the system U and
e(U)C£{<U,Nu{d 2 (<t>)}>).
Proof: Let U =< U, N > be a locally finite nonmonotonic rule system such
that a sentence e U appears in every extension of the system. Let d 2 (<j>) be the
strong refined common derivation of (j) as defined in Definition 3.1.29. Recall that
d 2 (<f>) = VtPin) : /\ R{r % ) U /\(P(r z ) A [\/ R{r t )])/ct>.
i i
We need to show that the premise of the rule is in every extension of the system U
and that no restraint is in any extension of the system. Let S be any extension of U.
First, consider the premise, VjPfa). Since S is an extension and thus <j> is in 5, we
have that there is a minimal proof scheme, p { € Dr^ that applies in S and concludes
(f). r t is the last rule of this proof scheme and thus it must apply in S so that its
premise, P(n) is in 5. Thus, \/ l P(r i ) is in S. Now we consider the set of restraints,
A^)uA(^)A{V^(n)D-
Since r { applies in S we have that no restraint in the set R(ri) is in S. Any a e
A, Rfc) has the form (5 X n A ... A (3 m jm where ^ g R{ ri ) for each i. Since ^. £ 5, it
48
follows that a £ S. Thus, no restraint in the set f\ t R(ri) is in S and P{r t ) A [V R{r l )}
is not in S. Thus, Ai(^( r i) A [V R{n)}) is not in 5 so that no restraints of d 2 {(f>) are
in 5. Thus, d%(4>) applies in every extension of the system U and therefore
e(u)cs(<u,Nu{d 2 {(j>)}>)
by Theorem 3.1.28.
Due to some of the same problems as before, we may still gain extra extensions
when the common derivation is added to the set N of rules. We now must ask if it
is possible to make sure that the sets of extensions will be the same, and if so, what
restrictions will be needed. We find that we can ensure that the sets will be equal,
and there are several options to do so.
Theorem 3.1.32 Let U —< U,N > be a locally finite premise-free nonmonotonic
rule system such that a sentence <j> G U appears in every extension of the system. Let
d 2 {<t>) be the strong refined common derivation of <f> as defined in Definition 3.1.29.
Then,
£{U)=S(<U,Nu{d 2 (d>)}>).
Proof: Suppose that U be a locally finite premise-free nonmonotonic rule
system and let 4> e U be a sentence that appears in every extension of the sys-
tem. Let d 2 (<f>) be the strong refined common derivation of as defined in Theorem
3.1.31. Then d 2 (0) =: A<(V^( r *))M B Y Theorem 3.1.31 we know that the common
derivation applies in every extension of U. Hence, by Theorem 3.1.31, we have that
£(W)C £(<[/, JVu{d 2 (0)}>).
We have only to show the reverse inclusion. For any consequence ip in some extension
S in the new system, there must be an S-applicable proof scheme for ip. If the last
rule in the proof scheme is anything other than d 2 (</>), then it is a rule of the original
49
system and therefore the proof scheme is valid in the original system. Otherwise,
d 2 ((f)) is the terminal rule of the proof scheme for ip and hence ip — 4> and this rule
applies in S so that Ai(V^( r i)) * s not m &• That is, for some *, (V R{ri)) is not in
S so that the premise-free rule r; applies in S. Hence, the proof scheme pi applies in
S. In either case, we see that any proof scheme in the new system is a proof scheme
in the original system. Therefore S is an extension of U, and
£{U) = £(<U,Nu{d 2 (<j ) )}>).
Note that in a premise-free system, all minimal proof schemes have just one
line. However, the requirements on the rule system need not be this strong, to ensure
that the sets of extensions will be the same. There are other options.
We then gain the following less restrictive results:
Theorem 3.1.33 Let U =< U,N > be a locally finite nonmonotonic rule system
such that any sentence in the intersection of all the extensions of the system is
premise-free. Suppose that a sentence (/> € U appears in every extension of the system.
Let dip be the standard common derivation of <j) as defined in Theorem 3.1.24- Then,
S(U)=£(U + ).
Proof: Let U =< U, N > be a locally finite nonmonotonic rule system such
that any sentence in the intersection of all the extensions of the system is premise-
free. Suppose that a sentence <j> E U appears in every extension of the system. Let
d^ be the standard common derivation of <j) as defined in Theorem 3.1.24. Then,
since the last rule in each proof scheme for <j> are the only rules considered in the
construction of the common derivation, we may follow the proof of the case of the
system U itself being locally finite and premise-free.
50
We may instead place the requirements on the sentence in question, i.e. on
the sentence which appears in every extension of the system.
Theorem 3.1.34 Let U =< U,N > be a locally finite nonmonotonic rule system
such that a sentence (j> 6 U appears in every extension of the system and is premise-
free. Let d/ be the standard common derivation of <j) as defined in Theorem 3.1.24.
Then, d^ 1 is premise-free and
£{U)=£{U + ).
Proof: Suppose that U =< U, N > is a locally finite nonmonotonic rule
system such that a sentence 4> € U appears in every extension of the system and is
premise-free. Let d/ be the standard common derivation of <j> as defined in Theorem
3.1.24. For any element a of the restraints of d/, a has the form l n A ... A /? m -
where p i ji E R(n) for each i, and no 1 h A ... A p m Jm is in S, for any extension S
in which the rule applies. We claim that for some i, none of the f3 l H is in S so that
the rule n applies. Supposing not, we may choose for each I some 5 t = f3 l in 5.
However, we then have that delta x A ... A 8 k e 5, a contradiction. Thus, any proof
scheme in the new system may be replaced with a proof scheme in the original system
and hence
£{U) = 8{U + ).
Next, we consider iterating the common derivation as in Chapter 2.
Considering the language to be infinite, and taking the common derivation
to be either the standard, refined or strong refined common derivation, we still have
that L x D l 2 D I 3 D.... We may define I* to be the intersection of all the J n , define
iV* to be the union of all the N n , and define £* to be the union of all the sets of
extensions of the rule systems <U,N n >. We then find the following:
51
Theorem 3.1.35 /• =()€*
Proof: Suppose that <f> e /*. Then, <j> € /„ for all n so that
<j>ef)£(<U,N n >)
for all n. Letting S be any extension in £* we have that 5 is an extension of <U,N n >
for some n so that (j) e S and thus € f]€*. For the reverse containment, suppose
that we have <j)Ef)£*. Then, <j> € S for any extension 5 g £* so that e S for any
extension S of any <U,N n >. Hence, </><=/„ for any n so that <f>ef)I n = I*. Thus
the equality holds.
Theorem 3.1.36 £* C 5(< £/, JV* >).
Proof: Let S € £* so that 5 is an extension of some < U,N n > and an
extension of any <U,N m > for m > n. We want to show that S is an extension of
< U, N* >. To do this, suppose that a rule r e N* generates for S. r e N m for some
m, and hence for some m > n. Since 5 is an extension of < U, N m > we have that
the consequence of r is in S so that S is an extension of < U,N* >.
One might ask at this point if we can show that iV* has common derivations
or if it does not. This is a point to be investigated.
3J2 Locally Finite Constructive Nonmonotonic Rule Systems
In this section, we consider the same question about nonmonotonic rule sys-
tems as in the previous section, but use a constructive approach. That is, we consider
that p Vq is not derived unless one of p or q is derived, and extensions are not closed
under the propositional rule p V ->p, as in the finite constructive case. Say that an
extension S is constructive if p V q e S implies that p e S or q 6 S. Note that if a
set S conatins p V -»p and is constructive, then S is complete.
52
Again, consider 0, a formula of the language L such that 4> £ f\S(U). Then
€ 5 for every extension S of U. As before, there is a finite list of minimal proof
schemes Dr^ = {px, . . . ,p m } that derive <j> in the extensions of U. For each t let r x be
the last (a.k.a. terminal) rule in p { . The advantage of the constructive approach is
the same as in the finite constructive case. It allows us to view each set of restraints
as a single formula instead of as a set of formulas. Then, instead of asking if each
element of the set of restraints is not in a context, we would ask if the restraint itself
is not in the context. As it stands, each rule r { has as its restraints the set {(3\,
...,/?* t .} for some /^ sentences of the language. We may instead let R(r t ) = f3\V ...
V(3\.. Then R(ri) is in an extension S if and only if /^ 6 S for some j. We find that
several of the theorems of the last section still hold.
Theorem 3.2.37 For any formula (j) of the language L such that <p e f]£(U), has
a common derivation d 1 ^ which generates (j) in each extension S of U where U is a
locally finite constructive nonmonotonic rule system.
Proof : Suppose U is a locally finite constructive nonmonotonic rule system.
Suppose further that is a sentence of U that appears in every extension of the
system. Since the system is locally finite, we have that there are only finitely many
minimal proof schemes for cf>. List the proof schemes for <f> as Dr^ = {p u ..., p m }.
Consider the last rule, r, = P(r\) : ft*, ..., &//</> of each proof scheme p z . Now, since
(f) appears in every extension of the system, we have that for each extension S, there
is a proof scheme that derives <f> in S, call it p s . Since each rule of the proof scheme
applies in S, we know that there must be a minimal proof scheme p t , for some i € {1,
..., m}, contained in p s that derives (/> in S. Let d$ be the nonmonotonic rule
ViP{n) : AiR(n)/<j>.
Let S be any extension of U. We only have left to show that d/ applies in S. Since
S is an extension of U, we have that there is some minimal proof scheme p { 6 Dr
53
that derives (f> in S. Since this proof scheme derives <j) in 5, each rule in the proof
scheme applies in S so that T{ applies in S. Thus, P(ri) G S and /V, ..., fi ti x ^ S.
Thus,
P{rt) = y l P(r l ) G 5
and any 6iA...AS m G AiRfri) will not be in S. Thus, d/ applies in 5 and concludes
c(d+ ) = (j>. Thus, for any formula (j) of the language such that <t> G p|£(^0> has a
common derivation d 1 ^ which generates <j> in each extension S oili. Note that rf 1 ^
may be in N, but then U + will have the same set of extensions as U.
As in the finite case, the classical and constructive locally finite versions of the
standard common derivation d 1 ^ produce very similar rules. The difference is that
the constructive version is computationally simpler. We may also simplify the strong
common derivation.
Theorem 3.2.38 For any formula <fi of the language such that G f)£(U), define
d\ to be ViP(r t ) : V i i?(r i )/0. Then,
d%€GD(JVu{d%},p|£(W)).
Proof : Let (j) be a formula of the language such that <f> G f]£(U). Consider
<f as defined above. Clearly d*^ G N U {d%}. Now, for every extension 5 in £{U)
we have that some minimal proof scheme Pi generates in 5 so that P(7\) G 5.
Thus, P{d* <t> ) = ViP{ri) G C[£{U). Lastly, we have that fl(d%) = \Z t R(ri) G f\£(U)
if and only if P(r,) G f|£(^0 f° r a ^ *■ However, this is if and only if R(ri) is in every
extension. Now let S Q be an extension where the rule r t generates. Then R(r t ) G S ,
a contradiction. So we have that R{d*^) is not in f]£(U). Thus d* $ generates <f> in
r\£{u).
By the same argument as in Theorem 3.1.28, we still have that £{U) C £(U + )
for any cj) G f]£(U). Also as before, we may gain extra extensions, i.e., the contain-
ment may be strict.
54
Further, we might try considering active nonmonotonic rule systems, in hopes
that this would cure the new system of its extra extensions. This does not help, just
at it did not help in the finite case, and for the same reasons.
However, all is not lost. The mission to attain equal sets of extensions for U
and U + is salvaged by returning to the refined common derivation di (</>). The only
required restrictions are that the system be locally finite and constructive.
Theorem 3.2.39 Let U —< U,N > be a locally finite constructive nonmonotonic
rule system such that a sentence <j> € U appears in every extension of the system. Let
di((f>) be the refined common derivation of as defined in Definition 3.1.29. Then,
£(U) = £(<U,Nl>{d 1 {<p)} >).
Proof: Let U —< U, N > be a locally finite constructive nonmonotonic rule
system such that a sentence <f> € U appears in every extension of the system. Let
di{4>) be the common derivation of <j> as defined in Definition 3.1.29. that S e £{U).
Then S is the set of ^-consequences in U of a subset I of U. To show that S €
£(< U,N U {di(<j))} >) we need to show that S is the set of S-consequences in
< U, N U {di(4)} > of some subset / of U. We let J = I . This is true as previously
since (p is in S and the only new rule concludes (p. Thus, we have only to show the
reverse inclusion. For any consequence ip in some extension S in the new system,
there must be an 5-applicable proof scheme for ip. If the last rule in the proof scheme
is anything other than di(<j>), then it is a rule of the original system and therefore
the proof scheme is valid in the original system. Otherwise, di((f>) is the terminal
rule of the proof scheme for ip and hence ip = <p and this rule applies in S so that
Ai(V- R (n)) is not in S. That is, for some i, (\/ R(n)) is not in S. Thus, no restraint
of di(4) is in S. Considering the premise of the rule, y l P(R l ), and knowing that the
premise is in S since this rule applies, we have that one of the P(R t ) is in S. This
55
is due to the system being constructive. Thus, the rule T{ applies in S. Hence, the
proof scheme pi applies in S. In either case, we see that any proof scheme in the new
system is replaceable by a proof scheme in the original system. Therefore S is an
extension of U, and
£{U)=£(<U,Nu{d 2 (<j>)}>).
Now we begin to question the usefulness of the standard common derivation
d l <p. This version still has its place. Under appropriate restrictions the less com-
plex (as compared to d\ (<j))) standard common derivation will yield the equal set of
extensions sought.
Theorem 3.2.40 Let U =< U,N > be a locally finite restraint-free constructive
nonmonotonic rule system such that a sentence <\> 6 U appears in every extension of
the system. Let d^ 1 be the standard common derivation of 4> as defined in Theorem
3.1.24. Then,
£(U) = £(U + ).
Proof: Suppose that U is a locally finite restraint-free constructive nonmono-
tonic rule system such that a sentence <j> e U appears in every extension of the
system. Let d+ be the common derivation of <j) as defined in Theorem 3.1.24. In this
case, d/ = Vi-Pfa) : I4>- By Theorem 3.1.24 we know that the common derivation
applies in every extension of hi. Hence, by Theorem 3.1.28, we have that
£{U) C £{U + ).
We have only to show the reverse inclusion. For any consequence ip in some extension
S in the new system, there must be an 5-applicable proof scheme for tp. If the last
rule in the proof scheme is anything other than d/, then it is a rule of the original
56
system and therefore the proof scheme is valid in the original system. Otherwise, d$
is the terminal rule of the proof scheme for tp and hence ip = <f> and this rule applies
in S. Considering the premise of the rule, ViP(i?j), and knowing that the premise is
in 5 since this rule applies, we have that one of the P{Ri) is in S. This is due to the
system being constructive. There are no restraints to worry about. Thus, the rule
rj applies in S. Hence, the proof scheme pi applies in S. In either case, we see that
any proof scheme in the new system is replaceable by a proof scheme in the original
system. Therefore S is an extension of U, and
€{U) = S{U + ).
It is important to note here that being restraint-free automatically makes the
rules monotonic, but that this case is still interesting in the context of what we are
trying to accomplish.
Theorem 3.2.41 Let U =< U,N > be a locally finite constructive normal non-
monotonic rule system such that a sentence (j) 6 U appears in every extension of
the system. Let d$ be the standard common derivation of (j) as defined in Theorem
3.1.24. Then,
£{U) = £{U + ).
Proof: Suppose that U is a locally finite constructive normal nonmonotonic
rule system such that the sentence 4> € U appears in every extension of the system.
Let dtf, be the common derivation of <j) as defined in Theorem 3.1.24. Then, d^ 1 =
VjP(rj) : ^/(j). By Theorem 3.1.24 we know that the common derivation applies in
every extension of U. Hence, by Theorem 3.1.28, we have that
£{U) C £{U + ).
57
We have only to show the reverse inclusion. For any consequence ip in some extension
S in the new system, there must be an S-applicable proof scheme for ip. If the last
rule in the proof scheme is anything other than d/, then it is a rule of the original
system and therefore the proof scheme is valid in the original system. Otherwise, d/
is the terminal rule of the proof scheme for ip and hence ip = 4> and this rule applies in
S so that -i0 is not in 5. Considering the premise of the rule, VjP(i?j), and knowing
that the premise is in S since this rule applies, we have that one of the P{Ri) is in S.
This is due to the system being constructive. Thus, the rule r, applies in 5. Hence,
the proof scheme p^ applies in S. In either case, we see that any proof scheme in the
new system is replaceable by a proof scheme in the original system. Therefore S is
an extension of U. Thus,
€(U) = £(U + ).
However, the requirements on the rule system need not be this strong, to
ensure that the sets of extensions will be the same. As in the classical case, there are
other options.
Theorem 3.2.42 Let U =< U, N > be a locally finite constructive nonmonotonic
rule system such that the intersection of all the extensions of the system is terminally
restraint-free. Suppose that a sentence (ft € U appears in every extension of the
system. Let d^ be the standard common derivation of 4> as defined in Theorem
3.1.24. Then,
€{U) = S(U + ).
Proof: Suppose that U is a locally finite constructive nonmonotonic rule
system such that the intersection of all the extensions of the system is terminally
restraint-free. Suppose further that a sentence </>£[/ appears in every extension of
58
the system. Let d^ be the common derivation of 4> as defined in Theorem 3.1.24.
Then, since the last rule of each proof scheme for (f> are the only rules considered in
the construction of the common derivation, we may follow the proof of the case of
the system U itself being locally finite, constructive and restraint-free.
Theorem 3.2.43 Let U =< U,N > be a locally finite constructive nonmonotonic
rule system such that the intersection of all the extensions of the system is terminally
normal. Suppose that a sentence (f> € U appears in every extension of the system. Let
d^ be the standard common derivation of 4> as defined in Theorem 3.1.24- Then,
£{U)=S{U + ).
Proof: Let U =< U, N > be a locally finite constructive nonmonotonic rule
system such that the intersection of all the extensions of the system is terminally
normal. Suppose that a sentence <f> € U appears in every extension of the system.
Let dj, be the standard common derivation of <j> as defined in Theorem 3.1.24. Then,
since the last rule in each proof scheme for (f> are the only rules considered in the
construction of the common derivation, we may follow the proof of the case of the
system U itself being locally finite, constructive, and normal.
Also as in the classical case, we may instead place the requirements on the
sentence in question, i.e., on the sentence (p which appears in every extension of the
system.
Theorem 3.2.44 Let U =< U,N > be a locally finite constructive nonmonotonic
rule system such that a sentence € U appears in every extension of the system
and is terminally restraint- free. Let d/ be the standard common derivation of <j) as
defined in Theorem 3.1.24. Then, d/ is restraint-free and
£{U) = E{U + ).
59
3.3 Characterizing The Set of Extensions
In the infinite case, we must again ask if, given a family of sets, we can con-
struct a nonmonotonic rule system whose set of extensions is exactly that family. The
unfortunate answer to this is no. Although the set of extensions of any nonmonotonic
rule system is noninclusive (i.e., forms and antichain), not every noninclusive family
of sets is the set of extensions for a nonmonotonic rule system. Consider the following
example.
Example 3.3.18 Let S = {{u t } : % = 0, 1, . . .}, that is, the family of all singleton
sets. This is clearly noninclusive. Now suppose that £ were the set of extensions of
some rule system U. For the extension {u }, there must be a proof scheme (j) with
finite support S and conclusion u . Now just choose some u k <fc S. Then (j) is also
applicable in {u k }, which means that {u k } is not deductively closed and is not an
extension.
The remedy for this is explored in the next chapter, where we are able to
successfully characterize the set of extensions of a locally determined nonmonotonic
rule system.
CHAPTER 4
LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS
In this chapter we consider a special nonmonotonic subcase of the infinte case.
We let U be a locally determined nonmonotonic rule system. This has a large impact
on the results.
4.1 Locally Determined Nonmonotonic Rule Systems
We may obtain a similar result in the case of U having infinitely many exten-
sions, if we make some adjustments. To do this, we will first need some preliminaries.
Let U =< U, N > be a countable nonmonotonic rule system. For simplicity,
we will assume that U is a subset of the natural numbers u) = {0,1,2,...}. Let
U = {u < t*i <... }.
The informal notion of a locally determined rule system U is one in which the
existence of a proof scheme for a sentence u { (or the lack of existence thereof) can be
determined by examining only rules or proof schemes involving some initial segment
oft/.
Given a proof scheme or a rule p, we write max(p) for the maximum of the
set {tjttj occurs in <j>}.
We shall write JV n for the set of all rules r e N such that max(r) < n and we
shall write U n = {u ,...,u n } and refer to the nonmonotonic rule system made up of
these two sets as < U n ,N n >.
Definition 4.1.45 Let U =< U,N > be a computable nonmonotonic rule system.
Say that n is a LEVEL ofU if for every subset S C {u , ...,«„} and alii < n + 1, if
60
61
there exists a proof scheme p such that the conclusion c(p) = U{, and R(p) 5 = 0,
then there exists a proof scheme q such that c(q) = Ui, R(q) C\ S — 0, and max(q) <
n+l.
Theorem 4.1.46 Suppose that n is a level ofU and suppose that E is an extension
ofU. Then, £ n = E D {u ,..., u n } is an extension of < U n , N n >.
Proof: Suppose that n is a level of U and suppose that E is an extension of
U. Let £ n — EC\{u ,..., u n }. Since E is an extension of U, then for any u, G £ n , there
is a proof scheme p such that the conclusion of p is Ui and the support of p has empty
intersection with E. Thus, in particular, the support of p has empty intersection with
£ n so that since n is a level, there exists a proof scheme p Q such that max(po) < n,
Po has conclusion Ui and the support of p has empty intersection with £ n . Thus, p
is a proof scheme of < U n ,N n >. In the other direction, if i < n and tt t £ £ n , then
there can be no proof scheme p of < U n ,N n > such that p has conclusion u t and
the support of p has empty intersection with £ n since this would violate the fact
that E is an extension of U. Thus, £ n is an extension of < U n , N n >.
Corollary 4.1.47 Suppose that n is a level of U and suppose that S C {u ,...,u n }
is not an extension of < U n , N n >. Then, there is no extension of E inU such that
ED{u ,...,u n } = S.
Further, say that U is LOCALLY DETERMINED or "has levels" if there
are infinitely many n such that n is a level of U. For a system U that is locally
determined, we let lev(U) be the set of all n such that n is a level of U and we write
lev(U) = {l < h <••• }•
Suppose that U is a recursive nonmonotonic rule system. Then we say that
the system HAS EFFECTIVE LEVELS if there is a recursive function / such that
for all i, f(i) > i and f(i) is a level of U.
62
Recall that a nonmonotonic rule system is said to be LOCALLY FINITE if for
each (j> e U, there are only finitely many ^-minimal proof schemes with conclusion <f>.
Recall also that U is HIGHLY RECURSIVE if U is recursive, locally finite, and there
is an effective procedure which, when applied to any (f> € U, produces a canonical
index of the set of all codes of -<-minimal proof schemes with conclusion <j>.
Now, a nonmonotonic rule system U that is locally determined is not neces-
sarily localy finite, but the set of extensions of U will nevertheless correspond to the
set of infinite paths through a finitely branching tree and similarly the extensions of
a nonmonotonic rule system with effective levels will correspond to the set of infinite
paths through a highly recursive tree.
Theorem 4.1.48 Let U =< U,N > be a recursive nonmonotonic rule system.
1. If U has levels, then there is a recursive finitely branching tree T and a
one-to-one degree preserving correspondence between the set of extensions S(U) ofU
and the set [T] of infinite paths through T. Also,
2. If U has effective levels, then there is a highly recursive finitely branching
tree T and a one-to-one degree preserving correspondence between the set of extensions
£(U) ofU and the set [T] of infinite paths through T.
Proof: There is no loss of generality in assuming that U — w so that u Q =
0,«i = 1,« 2 = 2,.... Next, observe that for each n, < U n ,N n > has only finitely
many minimal proof schemes so that we can effectively list all of the minimal proof
schemes p < p x <..., so that
1. If max(p k ) = i and max(p t ) = j and i < j, then k < I. (This says that if
i < j the the proof schemes whose maximum is i come before those proof schemes
whose maximum is j.)
63
2. If max(p k ) = max(pi) = i,k < I if and only if code(p k ) < code(pi) where
code(p) denotes the index assigned to a proof scheme p under some effective Godel
numbering of the proof schemes.
We shall encode an extension S of the system U by a path n s — (ftfe, jrj,...)
through the complete w-branching tree lu" as follows.
first, for all i > 0, n 2 i =s (*)• That is, at the stage 2i we encode the information
if i belons to the extension S. Next, if n 2 i = then 7r 2i+ i = 0. But if 7r 2i = 1 that
is, if t 6 S, then we put ir 2 i+i equal to that g 5 (z) such that p 9sW is the first minimal
proof scheme in our effective list of minimal proof schemes such that the conclusion
of p gs (j) is i and the support of p qs (i) has empty intersection with S.
Clearly S is turing reducible to ir s . For it is enough to look at the values of
its at even places to read off S. Now, given an 5-oracle, it should be clear that for
each i e 5, we can use an 5-oracle to find q s (i) effectively. This means that ir s is
turing reducible to S. Thus, the correspondence between S and n s is an effective
degree-preserving correspondence. It is trivially one-to-one.
The construction of a recursive tree T C lu" such that the set [T] of infinite
paths through T equals the set {n s \S is an extension of < U, N >} is given in
[MNR92b]. The key fact needed to establish the branching properties of the tree T
is that for any sequence a G T and any i, either a(2i) = a(2i + 1) = or a(2i) = 1
and a(2i + 1) codes a minimal proof scheme for i. We just note that when a proof
scheme p = a(2i + 1) does not correspond to a path tt s , then there will be some k
such that a has no extension in T of length k. This will happen once we either find
a smaller code for a proof scheme or we find some u > i in the support of the proof
scheme p such that all possible extensions r of a have t(2u) = 1.
Let L k = max({i\max(pi) < k}). It is easy to see that since the system U is
a recursive nonmonotonic rule system, we can effectively calculate L k from k.
64
We claim that the tree T is always finitely branching and that if the system
U has effective levels, then the tree T is highly recursive.
Clearly the only case of interest is when 2i + 1 < k and a(2i) = 1. In this
case we will let a(2i + 1) — c where the conclusion of the proof scheme p c is i and
the support of p c has empty intersection with l a and there is no a < c such that the
conclusion of the proof scheme p a is i and the support of p a has empty intersection
with I a . Now suppose that q is a level and that i < q. Then, by definition, there
must be a minimal proof scheme p such that max(p) < q, the conclusion of p is i and
the support of p has empty intersection with I a . Thus, p = p t for some I < L q . It
follows that c < L q where q is the least level greater than or equal to i. Thus, the
tree T is always finitely branching. Now, if the system U has effective levels which is
witnessed by the recursive function /, then it will always be the case that c < L f(l}
so that the tree T will be highly recursive.
Corollary 4.1.49 Suppose that the system U is a nonmonotonic rule system with
levels such that there are infinitely many n such that < U n ,N n > has an extension
S n . Then U has an extension.
Proof: Now consider the tree T constructed for the system U as in Theorem
4.1.48. Here we can again construct our sequence of minimal proof schemes p ,Pi, ...
recursive in U just as we did in Theorem 4.1.48. We can only conclude that the tree
T is recursive in the system U but in any case, T will be a finitely branching tree.
Now fix some level n and consider some m > n such that < U m ,N m >
has an extension S m . Then by the exact same arguement as in Theorem 4.1.46,
S n = S m n {0,...,n} will be an extension of < U n ,N n >. Now consider the node
a = (ct(0),... , a(2n + 1)) such that
1. a{2i) =0iU^S n ,
2. a{2i) = 1 ifieS n ,
65
3. cr(2z + 1) = if cr(2i) = 0,
4. a(2i + 1) = c where c is the least number such that max(p c ) < n, the
conclusion of p c is t and the support of p c has empty intersection with S n .
It is easy to see from our constuction of the tree T that a eT. It follows that
T is infinite and hence T has infinite path tt by Konig's Lemma. But the proof of
Theorem 4.1.48 shows that S^ is an extension of the system U.
The next quesion is how to ensure that we can get recursive extensions. In
particular, suppose that the set of extensions of U is a decidable n°i class, that is, the
set of infinite paths through a computable tree T with no dead ends. Then every node
of the tree has an infinite recursive extension. If we only assume that the set of dead
ends of T are computble, the any node with an infinite extension has a computable
infinite extension.
Definition 4.1.50 1. Let U =< U,N > be a nonmnotonic rule system with levels.
Suppose that {n\n is a level of < U, N >} = {/ < l x <...}. Then we say that
U HAS THE LEVEL EXTENSION PROPERTY if for all k, if S k is an extension
°f < Ui k ,N ik >, then there is an extension of S k+ i of < U tk+1 ,N lk+l > such that
Sk+i n {u ,...,ui k } = s k .
2. A level n ofU is a STRONG LEVEL ofU if for any level m < n ofU and
any extension S m of < U m ,N m >, if there is an extension S n of < U n , N n > with
S n ^ {uo,...,u m } = S m , then there is an extensions ofU with SCi {u ,..., u m } = S m .
3. U HAS STRONG LEVELS if there is a computable function f such that,
for each i, i < f(i) and f(i) is a strong level.
The level extension property provides a way to construct an extension of the
system U by extending from level to level. The following result is immediate:
66
Theorem 4.1.51 If E is a decidable U°i class of subsets ofU with levels, then there
exists a nonmonotonic rule system U with the level extension property such that E is
the set of extensions ofU.
Definition 4.1.52 We say that a recursive nonmonotonic rule system U with levels
has IMMEDIATE WITNESSES if for any levels m < n ofU, whenever there is a
set V C {u ,...,u m } such that there is an extension S ofU with Sn {u ,...,u m } = V
but there is no extension S ofU such that S fl {u ,...,u m+l } = V, then either
(i) there is a proof scheme p with max(p) < m such that the support of p is a
subset of {u ,...,u n } - V and p concludes u n+1 or
(ii) there is a proof scheme p with max(p) < n + 1 such that the support of p
is a subset of {u Q ,...,u n ,u n+1 } -V and the conclusion of p is in {u ,..., u n , u n+l } - V
(note: it is easy to see that it must be the case that u n+ i is in the support of p.)
One can extend this concept as follows:
We say that a recursive nonmonotonic rule system U HAS WITNESSES OF
DELAY k if for all n whenever there is a set V C {«„,...,«„} such that there is an
extension S of U with S D {u ,...,u n } = V but there is no extension S of U such
that S n {u Q ,..., u n+1 } = V, then either
(i) there is a proof scheme p with max(p) < n + 1 such that the support of p
is a subset of {tio,..., u n ) - V and p concludes u n+ i or
(ii) for all sets T C {u n+2 ,..., u n+k }, there is a proof scheme p T with max{p T ) <
n + k such that the support of p T is a subset of {u ,...,u n+k } - (T U V) and the
conclusion of p is in {u ,..., u n+k ) - (T U V).
Theorem 4.1.53 Suppose thatU is a recursive nonmonotonic rule system which has
witnesses of delay k for some k>\ and which has at least one extension. Then the
lexicographically least extension of the system is recursive.
67
Proof: We can construct the lexicographically least extension S of the system
U by induction as follows.
Suppose that for any given n we have constructed S n = SO {u ,..., u n ). Then
S n+ \ — S n unless either
(i) there is a proof scheme p of level n such that the support of p is a subset
of {u ,..., u n } — S n and p concludes u n+ i or
(ii) for all sets T C {u n+2 ,...,u n+ k}, there is a proof scheme p T of level n + k
such that the support of pr is a subset of {u ,..., u n+k } - (TuS„) and the conclusion
of pis in {u ,...,u n+k } - (TuS n ).
in which case S n+1 = S n U {u„+i}. Note that since there are only finitely
many minimal proof schemes of any given level, we can check conditions (i) and (ii)
effectively. Since there is an extension, it is easy to see that our definitions insure
that S n is always contained in the lexicographically least extension of the system U.
Thus, S = [j n S n is recursive.
By putting suitable effective bounds on the effective levels and/or the effective
witnesses, one can readily come up with conditions that force U to have exponential
time, NP, or P-time extensions. This is a topic of current research.
4.2 Common Derivations in Locally Determined Nonmonotonic Rule Systems
Let U =< U,N > be a nonmonotonic rule system with infinitely many ex-
tensions that is locally finite, locally noninclusive and locally determined (or "has
levels"). Suppose (j> G U appears in every extension of U. Since the system is com-
putable, we have that <j) - Uj for some j. Since the system is locally determined,
there are infinitely many n such that n is a level of U so that we may choose n{4>) to
be the least level of U greater than or equal to j. When we restrict each extension
of the system to the set {u Q , ...,u nW } we then have only finitely many extensions,
68
call them Si, ..., S m . Then we may define a common derivation df for in U to be
df =: {0 1 A.../\0 m \Vi,0 i € {«o, •• .,««(*)}, A £ £}/0-
We then get a result similar to the finite case.
Theorem 4.2.54 Let U =< U,N > be a locally finite, active nonmonotonic rule
system that is locally noninclusive and locally determined. Suppose a sentence $ € U
appears in every extension of the system. Let df be the common derivation of as
defined above. Then, df applies in every extension of the system U and
£(U)=£(<U,Nu{dt}>).
Proof: Let U =< U, N > be an active nonmonotonic rule system with in-
finitely many extensions. Suppose a sentence 6 U appears in every extension of
the system. Let d* be the common derivation of <f>. Consider an arbitrary restricted
extension Sj of U. Take any conjunction &A...AJ0U such that ft g S { . Then $ £ S 3
so that the conjunction $ x N...l\$ m in not in 5,- and thus none of the restraints of d* is
in S y Thus df applies in Sj and therefore it applies in every extension of the system
U. By Theorem 3.1.28 we now have that
£(U)C£(<U,Nu{dt} >).
To show that we retain the same set of extensions, we need only to show the reverse
inclusion. Suppose that So is a restricted extension of < U, JVU {d?} > that does not
extend to an extension of U. Then, since U is locally noninclusive, there exist %p u ...,
^ m € S such that ^ g 5,. Then, ViA...AV> m is a restraint of d* Thus, q^A-A^m
is not in 5 since df applies in 5 , a contradiction. Thus,
£(U) = S(<U,Nu{dt}>).
69
The other notions of the common derivation, the standard common derivation,
the refined common derivation and the strong refined common derivation developed
in chapter three still apply in locally determined nonmonotonic rule systems by the
same theorems.
4.3 Characterizing the Set of Extensions
In this section, we shall provide a characterization of the set of extensions of a
recursive locally determined nonmonotonic rule system U = (U,J\f). Let £{U) be the
set of all extensions of U. Our first observation is that S(U) is closed in the natural
topology on subsets of U.
Proposition 4.3.55 IfU is locally determined, then £{U) is a closed set.
Proof: Let Ei,E 2 , ... be a sequence of extensions with limit E in the usual
product topology on sets. Suppose that Ui G E. Then there must be some K such
that Ui G Ek for all k > K. Thus for each k > K, there is proof scheme 6 k such that
E k C\supp(9 k ) = 0. Now let / be the least level > i. Then since U is locally determined,
it follows that for each k > K, there is a proof <f> k of U\ such that E k n supp(<p k ) = 0.
But there are only finitely many possible support sets for such proof schemes in Ui
so that infinitely many of the (j) k have the same support S. However since SnE k =
for infinitely many k, it must be the case S D E = and hence u r e E. Vice versa,
suppose that u, ^ E. Thus there must be some K such that for all k > K, Ui £ E k .
Suppose by way of contradiction that there is proof scheme (f> with cln{(j)) — Ui and
supp(4>) = S with S n E = 0. Since S is finite, there must be some M such that
S n Em = for all m> M. But this would mean that </> would witness that u t G E m
for all m> M, contradicting our previous assumption. (This direction applies even
if U is not locally determined.) We should note however that, in general, £(U) is not
a closed set.
70
Example 4.3.19 Let U = {u , u u . . .} and let N consist of the following set of rules:
{ 2 u^ '■ Vn, A;}. This means that for any extension E and any k, u k 6 E if and
only if at least one of the set {u 2 k {2n+1) : n = 0, 1,. . .} is not in E. It is not hard to see
that for any k, there will be an extension E ofU which contains all of {u , u u ...,u k }.
Thus if £(U) were closed, then U itself would be an extension, which is clearly false,
since none of the rules are U -applicable. Hence £{U) is not a closed set.
We say that a family £ of sets is noninclusive if for any two sets A, B £ £ ,
neither A C B nor B C A. A second key property of the set of extensions of a
nonmonotonic rule system is that it must be noninclusive. That is, the following
holds.
Lemma 4.3.56 For any nonmonotonic rule systemU, the set £(U) is noninclusive.
However, not every noninclusive family of sets can be the set of extensions of
a nonmonotonic rule system. Recall the example given previously.
Example 4.3.20 Let £ = {{ Ui } : i = 0, 1, . . .}, that is, the family of all singleton
sets. This is clearly noninclusive. Now suppose that £ were the set of extensions
of some rule system U. For the extension {u }, there must be a proof scheme <j>
with finite support S and conclusion u . Now just choose some u k <£ S. Then 4> is
also applicable in {u k }, which means that {u k } is not deductively closed and is not
an extension. Thus £ = {{u t } : i = 0, 1, . . .} cannot be the set of extensions of a
nonmonotonic rule system.
However, by combining the two ideas of closure and noninclusivity, we can
define a condition which guarantees that a family of sets is the set of extensions of a
nonmonotonic rule system U = (U, N) with strong levels. Given a family S of subsets
of U, let S n = {E n {u , ...,u n }:EeS}.
71
Definition 4.3.57 Let S be a family of subsets ofU.
1. We say that n is a level of S if S n is mutually non-inclusive.
2. We say that S has levels if there are infinitely many n such that n is a level of
S.
3. We say that S has effective levels if there is a recursive function f such that,
for all i, f(i) > i and f(i) is a level of S.
There are many examples of families of set of U = {u , tti, . . .} with effective
levels. For example, consider the family S of all sets S such that for all n, \S n
{u , . . . , i4 2 "}| = n. It is easy to see that for all n, 2" is a level of S. For a more
general example, let U be the set of all finite truth table functions on a countably
infinite set {a ,a u ...} of propositional variables. That is, for each sentence ip of
propositional calculus, U contains exactly one sentence logically equivalent to %jj.
These are listed in order of the maximum variable a k on which the sentence depends.
Thus, uq and U\ are the (constant) True and False sentences; u 2 and u 3 are the
sentences a Q and -*a , u 4 , . . . ,ui 5 list the sentences depending on a and a l5 and so
on. Now let T be any consistent set of sentences and let S(F) be the set of complete
consistent extensions of T. The levels of 5 = {UnS : 5 6 S{T)} are just the numbers
2 2 - 1. This is because if two sets in S disagree on the first 2 2k - 1 sentences, then
there must be some t with i < k such that they disagree on a t , which means that
one of the sets contains a* but not ->ai whereas the other set contains -la, but not a { .
Thus the two sets are mutually noninclusive.
Theorem 4.3.58 IfS is a closed family of subsets ofU with levels, then there exists
a nonmonotonic rule system U with strong levels such that S is the set of extensions
ofU. Furthermore, if S is a decidable Yl\ class and has effective levels, then U may
be taken to have effectively strong levels.
72
Proof: Given the family S, we shall directly construct a nonmonotonic rule
system U = (U, N) such that 8{U) = S. First, if S is empty, we let N consist of the
single rule *** It is easy to see in this case that U has no extensions.
Thus we assume that S / and hence that each S n is nonempty as well. We
then create a set of rules for every level n of S. For each level n, let E?, . . . , ££ be the
list of all sets of the form En{u Q , ...,u n } for E £ S. Then for each such E? and each
c € £?, iV will contain a rule r t<c = &*£&* w h e re {A, . . . , m } = {u , ...,u n }- Ef.
It is then easy to see that each E™ is an extension of U n and that n is a level U n .
Moreover it easily follows that the set of extensions of U is exactly S.
For the second part of the theorem, we use the same nonmonotonic rule sys-
tem. We note that decidable n°-class of sets has the property that there is a highly
recursive tree T contained in {0, 1}* such that set of infinite paths through T corre-
spond to the characteristic functions of elements of S and T has no dead ends, i.e.
every node 77 € T can be extended to an infinite path through T. Thus for any level
n of <S, the sets EJ, . . . , E% n described above will just correspond the set of nodes of
length n in the tree T. Because each of the nodes of length n can be extended to
infinite path through T, it follows that each extension E? of U n can be extended to
an extension E of U such that £n{%...,u„} = £f. It then easily follows that n
is a strong level of U. Thus U will have effectively strong levels in this case.
One problem for nonmonotonic rule systems is to determine which sets of
extensions can possibly result from some (recursive) nonmonotonic rule system. It is
well known that any set of extensions must be mutually non-inclusive, that is, if S
and So are two different extensions of the system U, then we can never have S C Sq
or S C S. We will sometimes say that the set of extensions has the noninclusive
property. On the other hand, for infinite languages, not every mutually non-inclusive
set of extensions can be realized.
73
Nonmonotonic rule systems with levels may be used to produce a large family
of possible sets of extensions. Given a family F of subsets of U, let F n = {S n
{u ,..,u n }\S G F}.
Definition 4.3.59 Let F be a family of subsets ofU.
1. We say that n is a level of F is F n is mutually noninclusive.
2. We say that F has levels is there ar infinitely many n such that n is a level
ofF.
3. We say that F has effective levels is there is a recursive function f such
that for all i,i < f(i) and f(i) is a level of F.
Theorem 4.3.60 1. If F is a closed family of subsets of U with levels, then there
exists a nonmonotonic rule system U with levels such that F is the set of extensions
ofU.
2. If F is a decidable U°i family of subsets of U with effective levels, then
there exists a nonmonotonic rule system U with effective levels such that F is the set
of extensions ofU.
Proof: Observe that if F is empty, then there is a single rule : {u }/u with no
extensions. Thus, we may assume that F is nonempty and thus each F n is nonempty
as well.
For each level n, we have a set of rules as follows. For each S x , ...,S k list the
family of intersections Sn{%... , u n ] for S € F. For each partial extension Si and
each c € Si, we will have a rule r i|C with conclusion c and with restraints b for each
b <£ S t . We know that the rule r i<c must exist since Sj is not a subset of S z by the
noninclusive property.
74
We claim that each level n of the family F is also a level of the proof system
U. To see this, let T be a subset of {u ,..., u n }, let j < n and let p be a proof scheme
with conclusion Uj = en such that p has empty intersection with T. Since the rules
of U have no premises, we may assume that p consists of a single rule r = r^ c . Thus,
there exists S € F and a level m of F such that S t = S n {u ,...,u m }. If m < n,
then max(p) < m < n as desired, on the other hand, if m > n, then consider the
restricted partial extension S k = S D {u ,...,u n } and the corresponding rule r k}C as
level n. It is clear that S k C Si and that S k fl {u Q ,..., u n } = 5^0 {u Q ,...u n }. Then the
support of the rule r fc)C has empty intersection with 5 since max(rk, c ) < n and the
support of r fe)C is equal to {u ,..,u n } - S k = {u ,..,u n } -Si which is a subset of the
support of r, )C .
We need to show that the set of extensions of U is exaclty F. Let us first show
that any element S of F is an extension of the system U. Given c e S, the rule r ic
has no premises, has restraints all not in S, and has conclusion c. Thus, c has a one
line proof scheme. Next suppose that 5 admits some rule r — r k>d . If k = z, then of
course d G S, so that S is closed under r. If k ^ i, then by the noninclusive property,
r has a restraint b G Si - S k so that 5 does not admit r.
Next we show that U has no other extensions. Let S* be any extension of U
and suppose that it differs from each S £ F. Since F is closed, there must be a level
n such that S* = S* D {«<>,..., u n } differs from each SC\{u ,..., u n }. Otherwise, there
would exist, for each level n, some S n such that S* fl {u ,...,u n } = E n n {u ,...,u n }.
But then S* = lim n E n would be in F, since F is assumed to be closed.
Now there is at least one S G F n and S* * / S by the choice of n. Furthermore,
5* n {u ,..., u„} is an extension of < U n , N n >, by Theorem 4.1.48, since < U n , N n >
has levels. It follows that S* n {u ,...,u n } is not a subset of S, by the noninclusive
property, so that 5* n {w ,..., u n ) is nonempty. Thus there is some c GS* fl {u ,..., u n )
75
and therefore S* * admits some rule r i)C where S{ is an extension of F n . But then it
follows that S* n {uo,-..,u n } C Si, again violating the noninclusive property.
Suppose now that F is a decidable 11° i class and has effective levels. Then
for any n, we can compute the set of intersections S D U n for S G F, which will just
be the set of paths of length n in the tree T. Now we can effectively compute an
increasing sequence of levels and use the set of intersections S fl U n to compute the
rules at level n for the desired rule system.
It follows from the proof of Theorem 4.1.46 that if U has effective levels and has
the level extension property, then the family of extensions of U may be represented
as a decidable n°i class. Thus, we have the following results:
Theorem 4.3.61 1. Suppose that U is a recursive nonmonotonic rule system with
effective levels and has the level extension property. Then for every level n and
extension S n of < U n ,N n >, there is a recursive extension of S of U such that
Sn{u ,...,u n } = S n .
2. Suppose that U is a recursive nonmonotonic rule system with strong levels.
Then for every level n and extension S n of < U n ,N n >, if there is an extension S of
U with S n {uo,...,u n } = S n , then there is a recursive extension of S ofU such that
SD{u ,...,u n } = S n .
CHAPTER 5
COMPUTABILITY AND COMPLEXITY ISSUES
In this chapter we show a few results concerning the computability and com-
plexity of the common derivations and their associated nonmonotonic rule systems.
5.1 Finding Extensions with Low Complexity
Throughout this section, we shall assume that U = (U, N) is a recursive
nonmonotonic rule system such that U = u = {0,1,2,- ■ ■}. Moreover if U is locally
determined, we let {/ < h < . . .} denote the set of levels of U and if U has strong
levels, then we let {s < 5] < • • •} denote the set of strong levels of U.
In this section, we shall show how we can use the notions of levels and strong
levels to provide conditions which will ensure that U has an extension which has
relatively low complexity even when U is infinite. We shall distinguish two represen-
tations of U, namely the tally representation of U, Tal(U), and the binary represen-
tation of U, Bin(U). In the tally representation of U, we shall identify each n e U,
with its tally representation, tal(n), and in the binary representation of U, we shall
identify each natural number n with its binary representation, bin{n). Given a rule
r = Ql '-"' Q "^i'-" fl m > we let the tally and binary representations of r be given by
tal(r) = 2tal{a l )2---2tal{a n )3tal((3 1 )2---2tal{l3 m )3tal{ip) (5.1)
bin{r) = 2bin{a l )2 ■ ■ ■ 2bin(a n )3bin{p l )2 ■ ■ ■ 2bin(/3 m )3bin{tp) . (5.2)
We then let Tal{N) = {tal(r) : r e N} and Bin(N) = {bin{r) : r e N}. Similarly
given a proof scheme r/> = (0 X , . . . , <f> k ), we let the tally and binary representations of
76
77
ip be given by
tal(xp) = 4tal(<j> l )4 ■ ■ ■ 4tal(<f> n )4 (5.3)
bin(tp) = 4bin((/)i)4 ■ ■ ■ 4bin((j) n )4 (5.4)
Finally given a finite set of proof schemes proof T = {ipi, . . . ,tp s }, we let the tally
and binary representations of T be given by
tal(T) = 5taZ(V>i)5---5taZ(V>,)5 (5.5)
bin(T) — 56m(^i)5- • -56m(^ s )5 (5.6)
Definition 5.1.62 We say that the nonmonotonic rule system U is polynomial
time locally determined in tally, if the nonmonotonic rule system Tal(U) =
(Tal(u)), Tal(N)) has the following properties.
1. There is a polynomial time function g such that for any i, g(tal(i)) = tal(l ki )
where ki is the least number k such that l k > i.
2. There is a polynomial time function h such that for any i, h(tal(i)) = tal(Ti)
where Ti is the set of all proof schemes Ui k whose conclusion is i where tal(lk t ) =
g(tal(i))
Similarly we say that U is polynomial time locally determined in binary, if definition
(5.1.62) holds where we uniformly replace all tally representations by binary repre-
sentations. We can also define the notions of U being linear time, exponential time,
and polynomial space in tally or binary in a similar manner.
This given, we then have the following:
Theorem 5.1.63 1. Suppose that U is polynomial time locally determined non-
monotonic rule system in tally which has the level extension property. If I is a
level of U and Ei is extension of Ui such that there is a unique extension E of
U with E {0, ...,/} = Ei, then E e NP.
78
2. Suppose that U is polynomial space locally determined nonmonotonic rule sys-
tem in tally which has the level extension property. If I is a level ofU and Ei is
extension ofUi such that there is a unique extension E ofll with £Tl{0, ...,/} =
Ei, then E £ PS PACE
3. Suppose that U is polynomial time locally determined nonmonotonic rule system
in binary which has the level extension property. If I is a level of U and Ei is
extension ofUi such that there is a unique extension E ofli with £Tl{0, ...,/} =
E u then E <E NEXPTIME.
4- Suppose that U is polynomial space locally determined nonmonotonic rule sys-
tem in binary which has the level extension property. If I is a level of U
and Ei is extension of Ui such that there is a unique extension E of U with
EH {0,. ..,/} = E u then E € \J c > {DSPACE{2 nC ).
Proof: For (1), suppose that / = l t where recall that the set of levels oiU is
{lo < k < . . ■}■ Then for any i > l u consider the level Ik, where g(tal(i)) = tal(l k J.
By the level extension property, it follows that there is an extension of Uu , Ei. , such
that Eu n {0, . . . , /} = E t . Moreover, it must be the case that E n {0, . . . , l ki } = E tk
since otherwise we could use the level extension property to show that there is a
sequence of extensions {E^ : j > k{} such that for each j > hi, Ei is an extension of
U tj where E X] n {0, . . . , lj- X } — E Xi _ x . One can then easily prove that E' = Uj> ki E { . is
an extension of U such that E' n {0, . . . , /} = E t contradicting our assumption that
E is the unique extension of U such that E C\ {0, . . . , 1} = E t .
It follows that to decide if i € E, we need only guess Ei k ., verify that it
is an extension of Ui k , and check whether i G Ei h . We claim that this is an NP
process. That is, we first guess the sequence xe, (0)---X£, (4,) where xe, is
the characteristic function of Eu. Note that our conditions ensure that there is
some polynomial p such that l kt < p(\tal(i)\). It follows that we can compute l ko =
79
g(tal(0)),l kl = g(tal(l)), . . . ,l kl = g(tal(l ki )) in polynomial time in \tal(i)\. Since
for each j, l kj is the least level greater than or equal to j, it follows that l ko < l kj <
■• - hi. = hi- Thus if ki — s, we can find Z < ^1 < • • ■ < Z s is polynomial
time |ta/(t)|. Note by assumption, t < s. Now consider E r = Eu n {0, . . . ,Q for
r = t,t + 1,. . . ,s. By our definition of levels, it must be the case that each E T is
an extension of U lr . That is, if x £ E r , there can be no proof scheme ip oiU lr such
that cln(ip) = x and supp(ip) n E T — since otherwise ip would witness that x € E s .
Vice versa, if x e E r , then x € E, and hence there is a proof scheme 6 X of U is such
that cln(6 x ) = x and supp(6 x ) H E, = 0. But since / r is level, there must be a proof
scheme t/>* such that max(tp x ) < l r , cln(ip x ) = x, and supp{ip x )n(E s n{0, . . . , / r }) = 0.
Thus ip x is a proof scheme which witnesses that x £ E r . Note that if it is the case
that / r _! < x < l r , then ip x in r x . Thus since we can also compute h(tal(0)) =
tal{V ),h{tal(l)) a ia/(r x ),..., h{tal(l ki )) = tal(T llH ) in polynomial time in |ta/(i)|,
it follows that to check that E ik ^ is an extension, we need only verify that that for each
x > U, XE, k (x) = 1 iff there is a proof scheme tp x e T x such that supp(ip x ) n E lk = 0.
It is easy to see that for each such x our codings of proof schemes and rules is such
that we can decode tal(T x ) and check if there is such a i\) x is polynomial time in l ki .
Thus we can verify that E lk , is an extension of W Jfc . in polynomial time in \tal(i)\.
Hence it follows that E € NP.
The proof of part (2) is similar. However since in this case, the length of the
sequence xe,. (0) • • • Xe,. (ki) is bounded p(\tal(i)\) for some polynomial p, we do not
have to guess it. That is, in p(i) space, we check all strings of {0, l} /fc > to see if they are
the characteristic function of an extension E* of U ik such that E* n {0, ...,/} = E t .
Since there is only one such extension with this property, we can search until we find
it. Thus our computations will require only polynomial space.
The proof of parts (3) and (4) uses the same algorithms as in parts (1) and
(2). However in this case the string xe,, (0) • • • xe, (lk { ) may be also long a 2 p d 6in WI>
80
for some polynomial P. Thus the algorithm could take on the order of 2' w " (l) l c steps
in case (3) and require 2l 6in W |c space in case (4).
We should note that if we replace the hypothesis of polynomial time and
polynomial space by linear time and linear space in parts (3) and (4) of Theorem
(5.1.63) respectively, then we get the following.
Theorem 5.1.64 1. Suppose that U is linear time locally determined nonmono-
tonic rule system in binary which has the level extension property. If I is a level
ofU and Ei is extension ofUi such that there is a unique extension EofU with
En{0,...,l} = E h then E e NEXT.
2. Suppose that hi is linear space locally determined nonmonotonic rule system
in binary which has the level extension property. If I is a level of U and Ei is
extension oflii such that there is a unique extension E ofU with E'flfO, . . . ,1} =
Ei, then E <E EXPSPACE.
It is easy to show that we can weaken the hypothesis in Theorems (5.1.63) and
(5.1.64) that there is a unique extension E of U extending E t to the assumption that
there are only finitely many extensions of U extending E\ and obtain the conclusion
that all of the extensions of E t are in the same corresponding complexity classes.
However if we do not make any assumption about the number of extension of U which
extend Ei, then the only thing we can do is try to construct the lexicographically
least extension of E t . One can see that in cases (2) and (4) there would be no change
in the conclusion. However in case (1), the computations could take 2" c steps and in
case (3), the computations could require 2 2 " steps.
Finally we note that similar results can be proven using strong levels instead of
the level extension property. We state the appropriate definitions and results without
proof. Recall that if U has strong levels, then we let {s Q < s x < . . .} denote the set
of all strong levels of U.
81
Definition 5.1.65 We say that the nonmonotonic rule system U has polynomial
time strong levels in tally, if the nonmonotonic rule system
Tal(U) = (Tal(uj),Tal(N)) has strong levels and the following properties.
1. There is a polynomial time function g such that for any i, g(tal(i)) = tal(sk { )
where ki is the least number k such that s k > i.
2. There is a polynomial time function h such that for any i, h(tal(i)) = tal(Ti)
where I\ is the set of all proof schemes U Sk whose conclusion is i andtal{l k% ) =
g{tal(i))
This given, we then have the following.
Theorem 5.1.66 1. Suppose that U is a nonmonotonic rule system which has
polynomial time strong levels in tally. If I is a level ofU and Ei is extension of
Ui such that there is a unique extension EofU with E D {0, ...,/} = E t , then
E e NP.
2. Suppose that U is nonmonotonic rule system which has polynomial space strong
levels in tally. If I is a level ofU and E\ is extension ofUi such that there is a
unique extension EofU with E n {0, ...,/} = E h then E G P SPACE
3. Suppose that U is nonmonotonic rule system which has polynomial time strong
levels in binary. If I is a level ofU and Ei is extension ofUi such that there is
a unique extension E ofU with EC) {0, . . . ,1} = Ei, then E e NEXPTIME.
4- Suppose that U is a nonmonotonic rule system which has polynomial space
strong levels in binary. If I is a level of U and Ei is extension of Ui such
that there is a unique extension E of U with E n {0, . . . , /} = E t , then E 6
U C > (£>SP^C£(2" C )).
82
5.2 Computability and Complexity of Common Derivations
Corollary 5.2.67 Let < U, N > be a highly computable nonmonotonic rule system.
Then, for every sentence G f]E < u,N>, there exists a computable standard common
derivation d^ x that generates (f> in every extension of < U, N >.
Proof: Using the standard common derivation defined as in Theorem 3.1.24,
the definition of the rule yields an algorithm for constructing it. Since the system
< £/, N > is computable we have that each of U and N is computable so that the
set of minimal proof schemes, Dr^ for any sentence tp £ U is computable. Hence the
common derivation is computable.
Theorem 5.2.68 Let < U, N > be a highly exponential time (polynomial time, etc.)
nonmonotonic rule system. Then, for every sentence </> G f]E(< ty N >)> there
exists an exponential time standard common derivation d^ that generates </> in every
extension of < U,N >.
Proof: We use the same definition for the standard common derivation as in
Theorem 3.1.24. Since the rule system is highly exponential time, we have that the
set of minimal proof schemes, Dr^ may be computed in exponential time. Once this
is done, we need only to list the last rule in each proof scheme and construct the
common derivation. Since there are only finitely many proof schemes, the common
derivation may be computed in exponential time, i.e., in the time required to compute
the set of minimal proof schemes.
Theorem 5.2.69 Let < U,N > be a highly computable active nonomonotonic rule
system such that (f) appears in every extension of the system. If d/ is the standard
common derivation for <j> in < U, N > , then < U, N U {d/} > is highly computable
and active.
83
Proof: Suppose < U, N > is a highly computable active nonomonotonic rule
system and <j> appears in every extension of the system. Let d^ 1 be the standard
common derivation for 4> in < U, N > as previously defined, and consider the system
< U, N U {d^} >. This system is active and locally finite by Theorem 3.1.26. To
show that it is highly computable we have left to show that it is computable, and that
there exists an effective procedure which given any sentence ^ G U produces the set
Dr^ of minimal proof schemes for tp. The set U has not changed since we have added
no new sentences to the system by the addition of the common derivation. Thus,
U is still computable. Since the set N is computable, and the common derivation
is computable, we have that the set N U {d/} is computable. Thus, the system
< £/, TV U {d/} > is computable. Since the original system < U, N > is highly
computable we have that there exists an effective procedure which given any sentence
€ U produces the set Dr^ of minimal proof schemes for tp. This procedure is still
effective upon the addition of the common derivation to the set of nonmonotonic
rules of the system. Thus the new system < U, N U {d/} > is highly computable
and active.
Lastly, we find the following results as to the computability of the common
derivations di((f>) and d 2 ((f>).
Theorem 5.2.70 Let < U,N > be a highly computable nonmonotonic rule system.
Then, for every sentence <j> G f)E(< U, N >), the common derivations di(4>) and
^2(0) for 4> are computable.
Proof: The definition of each rule yields an algorithm for constructing it.
Since the system < U, N > is computable we have that each of U and N is computable
so that the set of minimal proof schemes, Dr,p, which is finite for any sentence ip G U,
is computable. Since these rules are constructed from the last rule in each proof
scheme, we have that they are computable.
84
Theorem 5.2.71 Let < U,N > be a highly exponential time nonmonotonic rule
system. Then, for every sentence <f> e f] E{< U, N >), the common derivations d x (0)
and ^(0) for <j> are exponential time.
Proof: Since the rule system is highly exponential time, we have that the set
of minimal proof schemes, Dr^ may be computed in exponential time. Once this is
done, we need only to list the last rule in each proof scheme and construct the rules
di((j)) and d 2 {(j>). Since there are only finitely many proof schemes, the rules may
be computed in exponential time, i.e., in the time required to compute the set of
minimal proof schemes.
Theorem 5.2.72 Let < U,N > be a highly computable active nonomonotonic rule
system such that (f> appears in every extension of the system. If d\ ((f)) is the common
derivation for (j) in < U, N >, then < U,N U {d x {<f>)} > is highly computable and
active.
Proof: Suppose < U, N > is a highly computable active nonomonotonic rule
system and appears in every extension of the system. Let d\(<j>) be the common
derivation for in < U,N > as previously defined, and consider the system <
U,NU {di{4>)} >. This system is active and locally finite by Theorem 3.1.26. To
show that it is highly computable we have left to show that it is computable, and that
there exists an effective procedure which given any sentence ip G U produces the set
Dr,p of minimal proof schemes for xp. The set U has not changed since we have added
no new sentences to the system by the addition of the common derivation. Thus,
U is still computable. Since the set iV is computable, and the common derivation
is computable, we have that the set TV U (di(#)} is computable. Thus, the system
<U,NU {di(<j))} > is computable. Since the original system < U, N > is highly
computable we have that there exists an effective procedure which given any sentence
85
ipeU produces the set Dr^ of minimal proof schemes for ip. This procedure is still
effective upon the addition of the common derivation to the set of nonmonotonic
rules of the system. Thus the new system <U,NU {di(#} > is highly computable
and active.
CHAPTER 6
ALTERNATE FORMALISMS OF NONMONOTONIC LOGIC
In this chapter we will discuss how the results of the previous chapters trans-
late into two particular formalisms of nonmonotonic reasoning, specifically Default
Logic and Logic Programming. We will treat each separately, begining with the nec-
essary definitions and preliminary theorems. Continuing, we show how each theory is
equivalent to nonmonotonic rule systems. Finally we will see how some of the results
of the previous chapters look through the eyes of these formalisms.
6.1 Default Logic: Preliminary Definitions and Theorems
Definition 6.1.73 A DEFAULT THEORY is a pair (D,W), where W is a set of
formulas of the language L, and D is a set of DEFA ULTS of the form d — A :
Bi,...B n /C where A, Bi,...,B n , and C are all formulas of the language L and the
default is interpreted as saying, "If A is true and B x , ..., B n are not contradicted,
then conclude C." Call A the PREREQUISITE of d, and write p(d) = ,4. Call
B x ,...,B n the JUSTIFICATIONS of d, and write J(d) = {B u ...B n }. Lastly, call C
the CONSEQUENT of d, and write c(d) = C. Note that it is possible for a default
to have no prerequisite and/or no justifications.
If E is a set of formulas of the language L, let Cn(E) denote the closure of E
under semantical censequence.
Now, if (D, W) is a default theory, and S is a set of formulas of the language,
call a default d GENERATING FOR THE CONTEXT S if p{d) is in S, and for all
(3 e J(d), -1/8 £ S. Let GD(D, S) be the set of all defaults in D that generate for the
context S.
86
87
Most simply, an EXTENSION, S, of a default theory (D, W) is a set of for-
mulas of the language L that is the smallest set T (by inclusion) such that T is
theoretically closed, i.e., T = Cn(T), T contains W, and for all defaults deD such
that p(d) 6 T and V/? € J(d), -i0 g S, c(d) e T [BDK97J. This last property is best
described as being "closed under the defaults of D."
Example 6.1.21 Let a, b, and c be atoms in the language L and let
D = {: {a}/b,: {c}/b,: {a}/^c,: {c}/^a}.
Then the default theory (D, 0) has two extensions:
S 1 =Cn({b,^c})
and
S 2 = Cn({b,^a}).
Moreover, we find that
GD(D,S l ) = {:{a}/b,:{a}hc}
and
GD(D,S 2 ) = {:{c}/b,:{c}/^a}.
Definition 6.1.74 Now, we may well-order the defaults of a default theory (D,W)
by some well- ordering <. We may then define AD± to be the set of all defaults in D
which are applied when the well- ordering is used to close W under the set of defaults.
This is done in the following way: we define an ordinal n < . For every e < n^ we
define a set of defaults AD, and a default d e . If the sets AD e ,e < a, have been
defined but r/x has not been defined, then
88
(1) If there is no default d E D\ \J £<a AD e such that:
(a) W U c(U,<o AD t ) h p(d)
(b) W U c((J e<Q AD e ) \f -■/?, for every <= J(d)
then rj^ = a.
(2) Otherwise, define d a to be the <-least such default de D\ (J e<Q AD £
Then set AD Q = (\J £<a AD £ ) U {d a }.
(3) Put AD±=\J e<1hi AD t .
Intuitively, we begin with the set W of formulas, and apply the defaults of D in
their order. Each time we apply only the ordering-least default which can be applied.
At some point (since the ordinal is well-defined [MT93]) there will be no available
dafaults that may be applied. At this point, AD± is the set of all defaults applied and
n^ is the number of steps needed to reach this stopping point.
Then, let T< be Cn(W U c{AD^)). This is the theory GENERATED BY <
Then, GD(D,T±) C AD± [MT93] so that
Cn{W U c(GD{D,T±))) C TV
Now, if< is a well-ordering of the defaults and for every (5 in J(AD^), ->/3 $ Cn(WU
c(AD^)) then T± is an extension of (D,W) [MT93]. That is, if
AD± = GD(D,T^),
then
2V = Cn(W U c(AD.<))
is an extension of(D,W). More precisely, ifT± = Cn(W Uc(GD{D,T±))), then T <
is an extension of (D, W). We now have that
(a) If S is an extension of (D, W) then there is some well ordering < of the
defaults in D such that S = Cn(W U c(AD±)) = Cn(W U c(GD(D,S))) [MT93J.
And,
89
(b) IfS = T± = Cn(W U c(AD±)) = Cn{W U c(GD(D, S))) for some well-
ordering :<, then S is an extension of (D, W).
Thus, S is an extension of (D, W) if and only if S = Cn{W U c(GD(D, S))).
Let £(£>,w) be the set of all extensions of the default theory (D, W). Call two
default theories {D u W x ) and (D 2 , W 2 ) EQUIVALENT, written (D u W x ) = (D 2 , W 2 ),
if they have exactly the same extensions, i.e., ifE(Dt,Wi) = ^(d 2 ,w 2 )-
Example 6.1.22 Let (D,W) be a default theory where D = {: /a -> 6} and W =
{a}. Then consider the default theory (£>', 0) where D' = {: /a -> b,: /a}. These two
theories are equivalent as they each have the same single extension
S = Cn({a^b,a}).
Theorem 6.1.75 (MT93) Let S C L. Then, S is an extension of (D,W) if and
only if S is an extension of (D U D , 0), where D = {: /^ g W}.
Proof : Suppose S is an extension of (D, W). Then,
S = Cn{WL)c(GD(D,S)))
which is clearly equal to Cn(0 U c(GD(D U D , S))) since each new default m D
will generate for any context S. Thus, each extension of (D, W) is an extension of
(DUD o ,0). For the same reasons, the converse also holds. Since they have exactly
the same extensions, the theories are equivalent.
Theorem 6.1.76 (MT93) Let S and S' be be two extensions for the default theory
(b, W). Then, ifSC S', then S = S'.
Theorem 6.1.77 (MT93) A default theory (D, W) has an inconsistent extension
if and only if Sent(L) is an extension and (D, W) has no other extensions.
90
!^2 Equivalence of Default Logic to Nonmonotonic Rule Systems
The equivalence of Default Logic to Nonmonotonic Rule Systems has been
shown by Cenzer, Marek, Nerode, Remmel [1999] and others. Here, we give the
equivalence as shown by Cenzer and Remmel. Let C be the prepositional language
underlying the given default logic. With C fixed, all our nonmonotonic rule systems
will have the same universe, namely the set of all well-formed formulas of C. We now
show how to interpret a given default theory as a nonmonotonic rule system.
Let (D, W) be a default theory. For every default rule r,
a: ft,..., ft
r =
7
construct the following nonmonotonic rule d r
. __ a : -"A,.. .,-■&
7
Next, for every formula ip e £, define the rule
d^ = —
i>
and for all pairs of formulas Xi»Xa define
Xl.Xl => X2 ■
m Pxux2 =
X2
Now define the set of rules N DfW as follows:
N D ,w = {d r :r e D} U {d^ : ip e W or ip is a tautology} U {mp XuX2 : X u X2 € £}.
We have the following result:
Theorem 6.2.78 [MNR90] Let (D, W) be a default theory. Then a set of formulas
S is a default extension of (D, W) if and only if S is an extension of nonmonotonic
rule system (U,N DfW ).
Theorem 6.2.78 says that at a cost of a simple syntactic transformation and additional
encoding of logic as (monotonic) rules, we can faithfully represent default logics by
means of nonmonotonic rule systems.
91
6.3 Previous Results Through the Eves of Default Logic
We will consider only those deafult theories which have at least one, but only
finitely many extensions. We will consider both the classical case and the constructive
case.
We consider a single default theory (D, W) that has a finite number of ex-
tensions and where D and W are at most countable sets. We intend to explore the
following question: If & is a formula of the language L, such that <f> € S for every
extension S of (D,W), then what, if anything, can be said about the theory and/or
the formula and its derivation in each extension.
Let D be the set {: /?/# e W}. Let D x = D Li D . We consider now the
default theory (A,0). This theory is equivalent to the original theory (D, W) since
they have the same set of extensions.
Theorem 6.3.79 For any formula <j> of the language L such that (f> 6 f| E (D,w),
has a common derivation d 1 ^ which generates 4> in each extension S of (D, W).
Proof: We prove the theorem using the equivalent default theory (£>i,0).
Then, since (D, W) and (A,0) have the same extensions, the theorem holds for
(£>, W). Suppose that is a formula of the language L such that 4> e f| s (£>i,fl)-
Then G 5 for every extension S of (D x ,0). Since each extension S is of the
form Cn(c(GD(D u S))), there must be, for each S, a finite set of defaults {d s u ...,
d s n } C D 1 such that {cid'i), ..., c(d° n )} h <f>. Define d iM by
i i i
Where we simply omit from the prerequisite conjunction those i for which d s t has no
prerequisite.
Claim 1: For any extension S of (A, 0), d {M € GD{D X U {d (0 , s) }, S)
92
Proof of claim 1: Let S be an extension of (A, 0). Consider d (0>g) as denned
above. Clearly d (0)4) £ JtyU^d^)}. Also,p(d (<M ) = AiPKi) G S since each p(d s ,) is
in S since each d s { must be applied to deduce <\> and therefore each d\ is in GD(D X , S).
Now, for every (3 in J(d {M ) = (J, J(d s l ), -i0 £ 5 since no /? in any of the J{d\) is
in 5. Thus, d (<M € GD(D X U {d (<M },S). Moreover, c(d (0 , s) ) = A*^,) deduces <j>
since {c(d*i), ..., c(d s n )} h 0. Thus, d { ^ } deduces in 5.
Now we have for each extension S of (A,0) a default d ( ^ s) which deduces
in 5. For any sets of formulas J u ...,J m define J x V...VJ m to be the set of disjunctions
{iiV...Vj m : jj £ J u i = l,...,m}. We then define d 1 ^ to be
k k k
V i=1 ?(<W : V i=1 J (^.))/V t=1 c (° ? (M)>
where S 1} ...,S* are all the extensions of the default theory (D, W). Call d ! the
COMMON DERIVATION of in (£>i,0).
Claim 2: d\ £ GD{D X U {d 1 ^}, S) for every extension 5 of (A, 0).
Proof of claim 2: Suppose that is a formula of the language such that <j> £
n s (»i,0)- Consider d 1 ^ as defined above. Clearly d\ £ D x U {d 1 ^}. Also, for any
extension S t of {D u fy, for all /3 in J{d ( ^ Si) ), -i/8 £ $ so that for every /? 6 J(d : ),
/? = iiV...Vj* where j, € •/(<*(*,*)) for each i = l,...,jfe. Then, for any extension $
of (A,0), -<0 € 5 t if and only if ->jiA.../\->j k £ Si, which implies that -ijy € $, a
contradiction. Thus, -.0 £ 5 for any extension S of (A,0). Lastly, p(d 1 ) 6 S for
any extension S of (A,0) since for any S, p{d (M ) £ S and p(dV) = \J s p{d {4> , s) ) .
Thus, (P 4 £ GD(D X U K },S) for every extension S of (£>i,0). Furthermore,
c(d^) = V s c(d(0 ia) ) deduces in every extension 5 since each c(d (0)S) ) deduces 4> in
5. Thus, for any formula of the language such that <f> £ f) E (Dl , 0) , has a common
derivation d 1 ^ which generates in each extension 5 of (A,0). Note that d 1 ^ may
be in D x , but then (D x u{d^},0) will have the same set of extensions as (D U Q), i.e.
(L>i U (d^},0) will be equivalent to (£>i,0). Further note that since d 1 ^ generates
93
for each extension S of (A,0), we have that it generates for the intersection of all
the extensions, that is, it generates for p|£(z>,w)- This completes the proof of Claim
2 and thus of the theorem.
Theorem 6.3.80 For any formula <j) of the language such that e f)T,( D}W) , define
d*^ to be
VMm) : U J (^))/ V c (<w-
s s s
Then, iff 6 GD(A U K }>n*W))-
Proof : Again, we prove the theorem using the equivalent default theory
(£>i,0). Since (D, W) and (2?i,0) have the same extensions, the theorem holds for
(D, W). Let be a formula of the language such that <f) <E f|^(Di,0)- Consider d%
as defined above. Clearly d% e D x U {cf%}. Now, for every extension 5 in E (Dl)0) we
have that d {M generates for S so that p(d (<M ) e S. Thus, p(d\) = \J s p(d {M ) €
fl s (£»i,0)- Lastly, for every extension 5 in E (£ , li0) we have that V/3 6 J(d {M ), ->/3 $ S.
Now, V/? € /(d%) = |J s J{d {4> , s )),Pe J(d {M ) for some extension 5 so that -./? £ 5.
Hence, -i/3 £ n s (0i,0)- Th us d% generates for f|S(D,,0).
Note that although this new default generates for the intersection of all the
extensions, it may not generate for each particular extension.
Example 6.3.23 Consider the default theory (D,0) where
D = {:{^a}/b,:hb}/a}.
This default theory has two extensions,
Si = Cn({b}),
and
S 2 = Cn{{a}).
94
We have that the formula a V b is in both of the extensions and we find that
d* a vb -■ {-a,^6}/aV6.
By the theorem, d* aX ,b generates for the intersection of the two extensions. However,
it does not generate for either of the extensions Si or S 2 since b £ Si and a € S 2 ,
respectively.
Since there are only a finite number of d\, there are only a finite number of
possible prerequisites, sets of justifications, and consequents of d^ s ). Thus there are
only a finite number of possibilities for d^ tS ) for each extension. Because of this, and
because we assume that the default theory has only finitely many extensions, we are
not in danger of having an infinite disjunction or union in d 1 ^ or in d*^.
Example 6.3.24 The common derivation of any formula (j) in (D, W) may not be
found in D or in W as this example illustrates. Let a, b, c be atoms in the language
and let
D = {: {a}/b,: {c}/b,: {a}hc,: {c)ha}.
Then the default theory (D, 0) has the two extensions
Si=Cn({b^c})
and
Also, as before,
and
S 2 = Cn({b,^a}).
GD(D,Si) = {:{a)lb,:{a}hc}
GD(D,S 2 ) = {:{c}/b,:{c}/^a}.
95
There is no default of D that derives b in both extensions. However, we may condsider
the common derivation of b in (D, 0) which is
d\ =: {a V c}/b V b =: {a V c}/b.
Then, d 1 b will generate b in each of these extensions.
Theorem 6.3.81 E( D ,w) C T,^ D u{d^},w) for any (j) 6 f| s (D,w)- Equivalently, E (Dl)0) C
£(D 1 u{dM,0), f or an y $ e fl s (»i,0)-
Proof : Suppose that i^ef) £(£>i,0) and suppose further that 5 is an extension
of (A, 0)- Then, (j) € S = Cn(c(GD(D u S))). We want to show that
5 = Cn(c{GD(D 1 u {d 1 *}, 5))).
Now, c(GD(D u S)) C ^(AuK^.S)). Thus, 5 = Cn(c(GD(A,5))) C
Cn(c(GD(Di U {d^},S))). We will now show that c(GD{D l U {d 1 ,},^)) C 5 =
CnWGDpx.S))). Let d 6 GD(D X U {d^.S). If d € A then d € GD{D U S)
so that c(d) € Cn(c(GD(A,5))) = S. If d £ D 1? then d = d J so that c{d) =
V s c K<m)- Now, d (<M generates for 5 so that c(d {<t>tS) ) e c(GD(D u S) and therefore
c(d) = \/ c (<W eS = Cn{c(GD(D 1 ,S))).
s
Thus, c{GD{D l U {d%}, 5)) C 5 so that S = Cn{c{GD{D l U {d\}, S))). Thus, 5 is
an extension of (D 1 U {d%},0), and E (Dl , 0) C E (DlU{d i 0}j0) .
The converse of this theorem is false. As the next two examples show, the
two default theories (D, W) and (Du {d 1 ^}, W) may be equivalent, but need not be.
That is, we may have that E(d,W) = E(Du{#a),W), but this is not always so.
96
Example 6.3.25 Consider the default theory where W = and D = {: {a}/b, :
{c}/b, : {a}/-ic, : {c}/->a}. 77izs de/au/^ i/ieory has two extensions:
Si=Cn({6,-c})
and
S 2 = Cn({b,^a}).
We found previously that b is in each extension and that the common derivation of b
in (D, 0) is
d\ =: {a V c}/b V b =: {a V c}/6.
4<tttn£ tf»w new default to D, we see that (D U {d\}, 0) has the same extensions S {
and S 2) since applying d\ does not prevent the application of any default in D.
Example 6.3.26 Now consider the default theory (D, 0) where
D = { Pl : / Cl ,p 2 : /c 2 , : {^a, -pi}/p 2 , : {-a, ^p 2 }/p u
■ hPi,^P2}/piVp2,Ci Vc 2 : {^Ci,-ic 2 }/a}.
This theory has two extensions,
S x = Cn({p 2 ,c 2 }),
and
S 2 = Cn{{p l ,c l }).
The formula c x V c 2 is in each extension and we find that
rf (ciVc 2 ,si) =P2 : /c 2 ,
and
97
so that
d\ivc 2 = Pi Vp 2 : /d Vc 2 .
77ien, Si andS 2 are both extensions of (DU {d l ClVC2 },®), but this default theory will
have a third extension
S 3 = Cn({p x V pa, d V c 2 , a}),
w/nc/i m noi an extension of the original default theory (£>,0).
In the previous example, S 3 is the only new extension obtained by adding the
common derivation to the set of defaults. To see this, let S be any new extension.
The common derivation must generate for S, else S is an extension of the original
system. Thus, we have that p, Vp 2 € S so that the conclusion c x V c 2 is in S as well.
If pi € S, then c : 6 S by the default p l : /c x so that Si C S, a contradiction to
the noninclusive property of extensions, since S is not an extension of the original
system. Similarly, if p 2 e S, then c 2 e S so that S 2 C S, a contradiction. Thus,
neither of pi or p 2 is in S. Also, if a is not in S, then the rule : {--a, ^p 2 }/pi applies
to conclude p, in S. Thus, ae5. From this we now have that S 3 C S so that S 3 = S
since extensions are noninclusive. Thus, there is only the one new extension.
Suppose we let I x be the intersection of all the extensions of the original default
theory (D,0). Then,
/i = Cn({(p 2 Ac 2 )V(p 1 Acj)}).
We consider the new dafault theory
(D 2 ,<b) = (Du{d\ lVC2 },$)
and the set I 2 of all conclusions common to every extension of (D 2 ,0). We find that
h = Cn{{( Pl V pa) A ( Cl V c 2 )}) C I x .
98
Moreover, we could choose a conclusion common to all the extensions of
(£) 2 ,0), such as p\ Vp 2 . This has the common derivation
rf2 piv P2 == I" 1 ** V -ipi, ->a V -<p 2 , ->a, -ip x V ->p 2 }/Pi V p 2 .
In any new extension S of
£>3 = (D 2 u{d 2 plVp2 },0)
that was not an extension of the theory (D 2 , 0), this common derivation must apply.
Similarly to the previous arguement, none of pi,p 2 ,c t or c 2 can be in S else we
contradict the noninclusive property of extensions. p\ V p 2 must be in S since the
common derivation applies. Thus, by the common derivation for C\ Vc 2 , we conclude
c\ V c 2 in 5 and thus a is in S by the appropriate rule from D. This is a contradiction
since the common derivation requires that a not be in S. Thus, there are no new
extensions, that is, (Z) 2 ,0) has the same set of extensions as (D 3 ,0).
On a different note, we may force the intersections I x and I 2 to be equal by
taking <p to be /\i\. This appears in every extension of (D,0). Letting
D 2 = (DLl{d 1 4> },®)
We find that if S is any new extension, then (j) € S since the common derivation must
apply (else S is not new). Thus,
h c h = h n S C /j
so that I\ = I 2 .
If we have a formula <f> appearing in some but not all the extensions of (Di, 0),
we may in the same fashion as Theorem 6.3.79 create a common derivation for that
will generate in each extension of (A,0) in which it appears. However, we find
that in this case Theorem 6.3.81 becomes false, as the next example illustrates.
Example 6.3.27 Let (D, 0) be the default theory where
D = {: {-iai, ->a 2 }/a 3 , : {-ia 2 , ->a s }/ai, : {-101, -ia 3 }/a 2 ,
Pi : {«l}/ci,Pa : {a 2 }/c 2 ,a 3 : /p, Vp 2 ,a! : /p u a 2 : /p 2 }.
21Wj £/ieon/ /ias as i/iree 0/ ate extensions,
Si = Cn({a 3 ,p l Vp 2 }),
5 2 = ^({02,^2,^}),
and
53 = CndaxiPua}).
We see that the formula c x V c 2 is in both S 2 and S 3 , but is not in Si. We find the
standard common derivation for c\ V c 2 to be
d l Cl vc 2 = Pi V p 2 : {ai V a 2 }/ci V c 2 .
,4ddma this new default to the set of defaults D, we find that both S 2 and S 3 are
extensions of the new default theory {D U {d\ lVC2 }, 0). S u however, is not an exten-
sion of (D U {d^jvcJJ) since it is no longer closed under the set of defaults. It is
important to note that 5 X is a subset of{a 3 , Pl Vp 2 , Cl Vc 2 } which is an extension of
(DUK C1VC2 },0).
Theorem 6.3.82 Let (£>i,0) be a default theory such that appears in some but not
all of the extensions. Consider d x to be the common derivation of (j> as defined m
Theorem 6.3.79. Then, for any extension S of {D u $), there is an extension S of
(A U {a%},0) such that S C 5. More specifically, if <f> e S then S = S and if
(j) £ S then S is strictly contained in S.
100
Proof: Suppose that (£>i,0) is a default theory such that tf> appears in at
least one, but not all of the extensions. Consider d x ^ to be the common derivation of
<\> as defined in Theorem 6.3.79. If <fi appears in only one of the extensions of (A, 0),
then the common derivation d 1 ^ is found in D x so that (D x , 0) = (D x U {d l <p}, 0), and
the theorem is trivially true. Thus, suppose that <j> appears in al least two exensions
of the default theory (Dj,0), but does not appear in every extension. Let S be an
extension of (£>i,0). If S is an extension of the new system (D x U {d 1 ^,®), we are
done. Also, if (j> is in S, then 5 is an extension of (D x U {d 1 ^},®) by the proof of
Theorem 6.3.81. Hence, consider the case in which <j> ^ S, and S is not an extension
of the new system (Di U {d 1 ^},©). Since S is an extension of (£>i,0), we have that
S = Cn(c(GD(D u S))). If d 1 ^ does not generate for S, then
GD(D l u{d 1 )P },S) = GD(D u S)
so that
S = Cn(c(GD{D l U{d l 4> },S)))
and thus S is an extension of the new system (D x U {d 1 ^}, 0), a contradiction. Thus,
d 1 ^ generates for S so that
<t> = c{d\) e c{GD{D l \J {d 1 ^}^)).
Let
S x =Cn(Su{d\}))).
Then,
Si = Cn{c{GD{D l U {d\},S)))
= Cn(c(GD(D 1 u{d\},S 1 ).
Thus, Si is an extension of the new system (D x U (d l *},0) and clearly S is strictly
contained in Si. Thus, if S is an extension of (£>i,0) then either S is an extension
101
of (Di U {d 1 ^},®) (in the case of <j) belonging to S) or S is strictly contained in an
extension of (Di U {d 1 ^},©) (in the case of not belonging to S).
Refering to example 6.3.26 we may consider any default theory (D, W), the
equivalent default theory (£>i,0) and the set
h =P|E (Dli0) .
Differently now, for every <f> in this set, we can find a common derivation d 1 ^ which
generates <f> in each extension S of {D u 0). Consider the default theory (D 2 , 0) defined
by
(AU{d%|0€/i},0).
We may then repeat the procedure to find
h = (|£(D 2 ,0),
and if this set is not empty, then we can find common derivations d% for each </> in
I 2 such that d 2 ^ generates in every extension S of (D 2 , 0). Then, we may condsider
the default theory (.03,0) defined by
(£> 2 u{d%|0e/ 2 },0).
We continue this construction by, assuming that D n is defined, let
In = £(D n ,0)-
Then, letting d% be the common derivation for <j> 6 I n in (D n , 0), we define D n+1 to
be
(I> B U{d%|*€/„},0).
This may be continued until 7 fc is empty for some k and/or D k = D t for all / > k
for some fc. This inductive definition begs the following questions. Is there a limit to
this process, i.e., is there always some k for which I k is empty and/or D k = D t for
102
all / > k? Does it make a difference if we work in the case where D and W are finite
versus countably or uncountably infinite? These questions should be investigated.
Example 6.3.28 Consider the first default theory of this section. Using this default
theory, we would find D 2 to be
D U {d\} = {: {a}/b, : {c}/b, : {a}/-*, : {c} ha, : {a V c}/b}.
{D 2 ,0) has the same extensions as (D, 0) so that I 2 = h = {b} and d 2 b = d l b . Then
Dk = D 2 for all k > 1.
Remark 6.3.83 By Theorem 6.3.81, we have thafL( Dl #) C S (D2i 0) C ... C S( Dn ,0) C
S(D n+1 ,0) Q ....
For a finite language, or just a finite i\, we must eventually have /„+] = /„
for some n. At this point, we find that we will have a common derivation in D n for
each <A € /„, when we consider D n to be defined using all of the common derivations
for conclusions in /„_!. (£>„,0) will be said to HAVE common derivations.
Theorem 6.3.84 For any default theory (£>,0) with finite I\ } there exists an n such
that (£> n ,0) has common derivations, and the default theory D n is equivalent to the
default theory D n+ k for any k.
For an alternate approach, we might consider the default theory (A,0) and
the set ii as before. However, we may choose one element from I x and define D 2
to be the default theory
(Au{dV},0)
as seen for Example 6.3.26. We may then consider the set of all formulas which
appear in every extension of D 2 , choose some ip among those, and define D 3 to be
(D 2 U{rf%},0).
103
We may continue in this way, however, we will keep with the previous construction.
Using either construction, and considering the language to be infinite, we still
have that I x D I 3 D /$ D.... We may define I* to be the intersection of all the /„,
define D* to be the union of all the D n , and define E* to be the union of all the sets
of extensions of the default theories (Z) n ,0). We then find the following:
Theorem 6.3.85 /• = f|E*
Proof: Suppose that <j> G I*. Then, 4> g I n for all n so that e f|E (Dn , 0)
for all n. Letting S be any extension in E* we have that S is an extension of (£>„, 0)
for some n so that <j> e S and thus e f)E*. For the reverse containment, suppose
that we have <j) € f] s *- Then, (f> e S for any extension S e E* so that $ € 5 for any
extension S of any (D n , 0). Hence, <£ € I n for any n so that (f>ef]I n = r. Thus the
equality holds.
Theorem 6.3.86 E* C E (D . )0) .
Proof: Let 5 6 E* so that 5 is an extension of some (D„,0) and an extension
of any (D m , 0) for m > n. We want to show that 5 is an extension of (D*, 0). To do
this, suppose that a default d G D* generates for S. d G D m for some m, and hence
for some m > n. Since S is an extension of (D m , 0) we have that the consequence of
d is in S so that S is an extension of (D*, 0).
It is known that the extensions of a default theory form an antichain. That
is, if Si C S 2 where 5 X and 5 2 are extensions of the same default theory (D, 0), then
Si = S3. Thus, the extensions of (D, 0), whether or not we take the constructive view,
form an antichain so that, assuming they are distinct, no one extension is contained
in any other extension.
The following results are of general interest.
104
Theorem 6.3.87 f\E {Dt9) D Cn(f[ s (c{GD{D,S)))).
Proof : For every extension S of (D, 0),
f]c(GD(D,S)) C c{GD{D,S)) C Cn(c(GD(D,S))) = S
s
so that f\ s c(GD(D, S)) C S. Thus, since each 5 € £(d,0) is a theory, we have that
f|£(D,0) is a theory so that Cn(f] s (c{GD(D,S)))) C f| E (D,0)-
Theorem 6.3.88 Cn(C\ s (c{GD{D,S)))) C Cn(c(GD(2), f| £(!>,»))) and tfiej, are
eaua/ »/ and only if f] £(d,0) = 5 /or a// extensions S, or
Vd € GD(D,n E (^))' V ^ € J(d),-,/? £ |J E (^)-
Proof: Let c(d) G fls^CD^, S))). Then, d G GD(D,S) for every ex-
tension 5 of (£>,0). Thus, for every extension 5, we have that p(d) G 5 and
V/3 G J(d),^(3 i S. So, p(d) G nS(D,e) and V/3 G J(d),-./? £ f|V»)' Th us,
dG G*D(D,flE(D,0)) so that c{d) G c(GD(D,ri£(o,0)))- Hence,
n(c(GD(D,5))) C c(GD(D,f|E (Di0) ))
5
so that
Cn(f](c(GD(D,S)))) C Cn(c(GD(D,f|E (D , 0) ))).
s
Now suppose that c(d) G c(G'D(D,nE (D)0) )). Then, d G GD(D,nS (Di0) ) so that
p(d) G D s (d,0) and V/? G J(d), -./? £ D 2 (d,0))- This means that p(d) G 5 for every
extension 5, but we do not necessarily have that V/3 G J{d),^/3 ^ (JE (Dj0) , the
necessary condition if we are to have that c(d) G DsW^tA S))). Now, if either
fl £-(£>,0) = 5 1 for all extensions 5, or
Vd G GD(£>,p|E Pi0) ),V/? G J(d),^3 £ U E W0)'
105
then then we would have that c(d) 6 f\ s (c(GD(D, S))). Then,
c(GD(D, f|S(D,0))) C f\(c(GD(D,S)))
s
so that
Cn(f](c(GD(D,S)))) = Cn(c(GD(D, f]j^, m ))).
s
Clearly, if Cn(f] s (c(GD(D, S)))) = Cn(c(GD(D, fl^W)), then either ft E (D , 0) =
5 for all extensions S, or
Vd € G-D(£>,n s (^))> V /? 6 .7(d), -0 £ |J E (^)-
Example 6.3.29 Let D = {: /p,p : {a}/e,p : {^a}/-a}. 77jen, (fee de/aw/£ i/ieory
(D, 0) /ms i/ie extensions
and
so that
and
Then,
but
S l =Cn({p,e})
S 2 = Cn({p, -na})
GD(A5 1 ) = {:/p > p:{a}/c}
GD(D,5 2 ) = {:/p,p:{^ a }/-a}.
GD(D,S l )nGD(D,S 2 ) = {: /p],
GD(D, Si n 5 2 ) = G£>(D, {p}) = D
since p e {p} and neither -.e nor a is in {p}. We then see that
c(GD(D, 50) n c(GD(D, S 2 )) = {p} ± {p, e , ^ a } = c(GD(D, 5, n 5 2 )).
106
Hence,
Cn(c(GD(D, 50) n c(GD{D, S 2 ))) = Cn({p})
? Cn(c(GD(D, S 1 nS 2 ))) = Cn({p, e, -a}).
Corollary 6.3.89 Cn(f) s (c(GD(D,S)))) = Cn(c(GD(D,f]i: {D ^))) ,i/(£>,0) is a
justification free default theory.
Proof : Suppose (Z>,0) is a justification-free default theory. Then, the stan-
dardized theory {D, 0) is also justification-free. Then,
W € GD(D,p|£ (i) , 0) ),V/? 6 /(d), ^3 £ |JE (D , 0)
since there does not exist /? G J(d). Thus,
Cn(f|(c(GD(D,5)))) = Cn(c(GD(D,f|E {/3 , 0) ))).
s
Note that a justification-free default theory is monotone, but the nature of
the result is still interesting.
We now take the case of constructive default theories. Again, consider a
single default theory (D, W) where D and W are at most countable sets. In this
section, we consider the same question about default theories as previously, but use
an constructive approach. That is, we consider that pVq is not derived unless one of p
or q is derived. Before considering the theory as is, we first "standardize" the theory
as we did previously to a more suitable one (£>i,0). This is done in the following
way:
Let D be the set {: /V# e W}. We consider now the default theory (D x , 0)
Where D x = D U D . This theory is equivalent to the original theory (D, W) since
they have the same set of extensions [MT93].
107
Again, we consider 0, a formula of the language L such that € fl^Di,!).
Then e S for every extension S of (A,0)- Since each extension S is of the
form Cn{c{GD(D u S))), there must be, for each S, a finite set of defaults {d s x ,
..., d s n ] C Di such that {c^), ..., c(d s n )} h 0, as before. The advantage of the
constructive approach is that it allows us to view each set of justifications as a single
formula instead of as a set of formulas. Then, instead of asking if each element of the
set of justifications is not contradicted in a context, we would ask if the justification
itself is not contradicted in the context. As it stands, each default d s t has as its
justifications the set {/3\, ...,^ k } for some ff i i formulas of the language. We may
instead let J(d s i) = 0\A ... A/?Y Then ^J(d°i) = -./^ v ... v-./3\ is in the extension
S if and only if -./^ g S for some j, a contradiction since each d s { generates for S.
Thus, we have that for each extension S, -. J(d s l ) <£ S for each *. We find that several
of the theorems of the last section still hold.
Theorem 6.3.90 For any formula (f) of the language L such that 6 f]T, (DM1 ,
has a common derivation d 1 ^ which generates in each extension S of(D,W).
Proof : We prove the theorem as before using the equivalent default theory
(£>i, 0)- Then, since {D, W) and (A, 0) have the same extensions, the theorem holds
for (D, W). Suppose that is a formula of the language L such that 6 n s (o,,0).
Then there must be, for each extension S, a finite set of defaults {d s x , ..., d s n } C D x
such that {c(d\), .., c(d s n )} h 0. Define e/ (<M by
t i i
Claim 1: For any extension S of (£>i,0), d {M e GD(D X U {d i</>tS) } , S)
Proof of claim 1: Let S be an extension of [D u $). Consider d {M as
defined above. Clearly d {M € D x U {d (0!i) }. Also, p(d {4> , s) ) = AiP(rf'i) € 5 since
108
each p(d s i) is in S since each d s { must be applied to deduce <j> and therefore each d\
is in GD{D U S). Now, for this extension S of {D u 0), -J(d (<M ) = -.(/^ J(rf s 2 )) g 5
if and only if Vj^-A^i)) € 5. Because of the constructive view we are taking, this
cannot happen unless ^J(d s i) G S for some i, a contradiction since -^J{d s i) <£ S
for each i. Thus, ->J{d {M ) £ 5. So, d {M G ££>(£>! U {d (0 , a) },S). Moreover,
c(d (<M ) = Ai c ( rfs i) deduces since {c^), ..., c(d s n )} h 0. Thus, d (0ii) deduces
in 5.
Now we have, as in the last section, for each extension S of {D u 0) a default
rf(0 )S ) which deduces in 5. Define rf 1 ^ to be
V r p(d(*,«)) = V ' J{d {M )l\lc(d ( ^ s) ).
s s s
Call d 1 * the COMMON DERIVATION of in (A,0).
Claim 2: d% G G?D(A U {d%}, 5) for every extension 5 of (A, 0).
Proof of claim 2: Suppose that is a formula of the language such that <j> G
fl s (£>i,0)- Consider d 1 ^ as defined above. Clearly d 1 ^ G D x U {d 1 ^}. Also, for any
extension S of (A,0), -J(dV) = - V, M<m) 6 5 o if and only if f\ s {^J(d iM )) £
S . However, this is if and only tf->J(dfa ao) ) G S , a contradiciton. Thus, ^J(rf ! ) f|
5 for any extension 5. Lastly, p(d x ) G 5 for any extension S of (A,0) since for
any 5, p(d (0i4) ) G 5 and p(d%) = \J s p( d (*,*)) ■ Thus, d 1 * G GD{D l U {d^}^) for
every extension 5 of (Di,0). Furthermore, c(g^) = V s c(d (<M ) deduces in every
extension 5 since each c(d^ f8) ) deduces in 5. Thus, for any formula <j> of the
language such that G fj^Di § has a common derivation d 1 ^ which generates
in each extension 5 of (Z?i,0). Note that d 1 ^ may be in D u but then (D, U {d\, 0)
will have the same family of extensions as (D u 0).
Theorem 6.3.91 For any formula (j> of the language such that (/) G f\E( DtW ), define
d% to 6e V>(<W : A a J(d iM )/\/ a c(d {M ). Then,
<r*€GD(AU{d%},f|E (iW ).
109
Proof : Again, we prove the theorem using the equivalent default theory
[Di,$). Since (D,W) and (A,0) have the same extensions, the theorem holds for
(D, W). Let be a formula of the language such that (j> G f| s (Di,0)- Consider d*
as defined above. Clearly d% £ D x U {d%}. Now, for every extension 5 in E tDl>0) we
have that d (0>4) generates for S so that p(d (0>s) ) e S. Thus, p(d%) = V s p{d {4><s) ) S
D s (Di,0)- Lastly, we have that -«J(d%) = ^ f\ s J{d {4>>s) ) € f| E (D,vv) if and only if
V s h J ( d (4>,s))) 6 HW)' However, this is if and only if -nJ(d {<f> , So) ) 6 f|£(/W)
for some extension 5 . Then, ^J(d (( ^ o) ) e S , a contradiction. So we have that
-"•/(d**) ^ n s (o,w)- Thus d* generates for f| s (Oi,fl)- Moreover, cid*^ = c^)
generates <j) in every extension so that c(d* c/> ) generates <j> in f\E(D,wy
As before, since there are only a finite number of d s h there are only a finite
number of possible prerequisites, sets of justifications, and consequents of d ((M) . Thus
there are only a finite number of possibilities for d (<M . Because of this, we are not
in danger of having an infinite disjunction or conjunction in d 1 ^ or in d%.
Example 6.3.30 Consider the first default theory of this section. Under this ap-
proach, we let
D - {: a/b, : c/b, : a/->c, : c/->a}.
Then the default theory (D, 0) has the two extensions
and
Also,
and
Si=Cn({6,^c})
S 2 = Cn({b,^a}).
GD(D, S^ = {: a/b, : a/^c}
GD(D,S 2 ) = {:c/b,:c/^a}.
110
Just as before, there is no default of D that derives b in both extensions. However, we
may condsider the common derivation of b in (D, 0) by the methods of this section,
which is
d\ =: a V c/b V b =: a V c/b.
Then, d l b will generate b in each of these extensions. Compare this version of the
common derivation of b in (D, 0) to that of the previous section where we had
d\ =: {a V c]/b V b =: {a V c]/b.
We see that the two methods produce very similar results, but that the common deriva-
tion produced by the constructive methods of this section is computationally simpler.
By the same arguement as in Theorem 6.3.81, we still have that E (D ,w) C
£(DuK },ty) for any (j> £ f\T, {DiW) . Equivalently, E (Cl , 0) C E (DlU{d i 0}0) , for any
<j) G plE( £ , l! 0). Also as before, the converse of this theorem is false.
We may again inductively define the default theory (£> n ,0) as we did in the
last section. Investigations into the questions raised by this definition are further
warented in this setting as the common derivations are computationally simpler and
the constructive view may make the difference in what the answer to those questions
will be.
Example 6.3.31 Considering our basic default theory again, and the methods of this
section, we would find D 2 to be
A U {d\} = {: a/b, : c/b, : a/^c, : c/^a, : a V c/b}.
Again, (D 2 , 0) has the same extensions as (D, 0) so that I 2 = I x = {b} and d 2 b = d\.
Then D k = D 2 for all k > 1 .
Ill
Remark 6.3.92 As in the last section, we will have that 2(^,1) C £(/>,,!) C ...
Q s (Dn!0) C E {Dn+li0) c ....
When considering the finite constructive case, we may be sure that it is still
interesting in the case of default logic by considering the two atom case as we did
before. Here, there is a bit more to say.
When considering a constructive view of the default theories, we must ask to
what extent this view weakens the results. That is, by using a constructive view,
what families of possible extensions are excluded and does this exclusion cause the
subsequent theory to be uninteresting. In this section we examine the case where the
language has two atoms, p and q.
Any extension of a default theory must be a theory in the language. There
are fifteen possible extensions which may be partially ordered by implication. They
are:
Cn(p A q), Cn{p A -. g ), Cn{^p A q), Cn{-^p A -.g), Cn(p), Cn{q), Cn(-p),
Cn{^q), Cn(p <—> q), Cn{p ♦— > -, 9 ), Cn(pV q) , Cn(pV-^q), Cn(-<pVq), Cn(^pV
Now, for any default theory we have that no one extension is contained in
any other extension. This greatly limits the possible sets of extensions that any one
default theory in this language can have. To see the possibilities more easily, we make
the following definitions:
A = {Cn(p V q), Cn(p V -.g), Cn{^p V q), Cn(^p V -- 9 )}
B = {Cn(p), Cn(q), Cn(-ip), Cn(-qf), Cn(p ^-> q), Cn{p f— ► -, g )}
C = {Cn{p A q), Cn(p A -.g), Cn{^p A q), Cn(^p A -q)}
112
Taking the constructive view, we cannot derive any element of A and we
cannot derive either of Cn(p i — ► q) and Cn(p < — ► -<q). Without the constructive
view, there are 141 possible families of extensions coming from:
15 subsets of A, 63 subsets of B, 15 subsets of C, 12 families having one
element from A and one element from B, 6 families having two elements from A and
one element from B, 12 families having one element from B and one element from
C, 6 families having one element from B and two elements from C and 12 families
having two elements from B and one element from C.
Taking the constructive view, we eliminate all but 46 of these possible families
of extensions. We allow only 15 of the subsets from B, all of the 15 subsets from C,
8 families having one element from B and one element from C, 4 families having one
element from B and two elements from C, and 4 families having two elements from
B and one element from C. We should note that any default theory whose family of
extensions is a singleton is a monotone theory
The resulting mathematics remains interesting as for any of the 46 possible sets
of extensions we can find a default theory with exactly those extensions. Specifically,
for any acceptable family F = {Cn(7\)„ ..., Cn(T n )}, the default theory (D, 0) where
D = {= hW * i}/T t \l < i < n}
will have F as its set of extensions. For example, for the family {Cn(p),Cn(q)} we
would choose the default theory
({: ->g/p,:-np/g},0).
This default theory will have exactly the two theories Cn(p) and Cn(q) as its exten-
sions.
Now, since the intersections of families of extensions is of particular interest,
we might ask which acceptable families of extensions have intersections which yield a
113
specific theory. Knowing this, given a theory which we desire to see as the intersection
of extensions we may create the default theory whose extensions intersect to yield
that theory.
In the two atom case, intersections of families of extensions proceed as follows:
Cn(p A q), Cn(p A ->q), Cn(^p A q), and Cn(^p A -.<?) are the intersections
of only themselves. The other ten theories (aside from Cn(true)) can be seen as
intersections of the following families:
Cn(p) = f]{Cn(p)} = f]{Cn(p A q),Cn(p A -<?)},
Cfl(-V) = f|{Cn(-p)} = f]{Cn(^p A q), Cn(^p A -,<?)},
Cn(q) = f]{Cn(q)} = p\{Cn(p A q), Cn(^p A q)},
CnH) = f]{Cn(^q)} = f]{Cn(p A -y), Cn(^p A -*)},
Cn{p < — > q) = f]{Cn(p A q), Cn{^p A ^q),
Cn(p < — > ^q) = f]{Cn{p A - 9 ), Cn(-p A q)},
Cn(p Vq) = (~){Cn(p), Cn(q)} = f]{Cn(p A q), Cn{p A -.g), Cn(-* A 9)},
Cn(p V -g) = f|{Cn(p), Cn(-g)} = f|{Cn(p A q), Cn(p A -.9), Cr^-^ A -.?)},
Cn(-p V 9 ) = f|{Cn(-np), Cn(g)} = f|{Cn(p A ?), Cn(-p A q), Cn(-,p A -*)>,
Cn(^p V -.9) = f|{Cn(-.p), Cn(-g)} = (~){Cn(p A -.g), Cn(^p A g), Cn(-*> A -*)}.
So we see that any given theory may be derived as the intersection of a set of
acceptable extensions.
114
6.4 Logic Programming: Preliminary Definitions and Theorems
The stable model semantics of logic programs has been extensively studied.
Unfortunately, the set of stable models of a recursive prepositional logic program with
negation or even of a finite predicate logic program with negation can be quite be quite
complex. For example, in [MNR90], it is shown that for any recursive propositional
logic program P, there is an infinite branching recursive tree T P such that there is
an effective 1:1 degree preserving correspondence between the set of stable models
of P and the set of infinite paths through T P . In [MNR92a] it is shown that given
any infinite branching recursive tree T, there exists a recursive propositional logic
program P T such that there is an effective 1:1 correspondence between the set of
infinite paths through T and the set of stable models of P. Moreover, in [MNR92a],
it is shown that the same result holds if we replace recursive logic programs by finite
predicate logic programs with negation. These results imply that the set of stable
models of a recursive propositional logic program or a finite predicate logic program
can be extremely complex. For example, it follows from these results that there a
finite predicate logic program which has a stable model but has no stable model which
is hyperarithmetic. The main motivation for this paper was to develop conditions
on recursive logic programs P which would guarantee the existence of well behaved
stable model for P, i.e. a stable model of P which is recursive or possibly even
polynomial time.
We shall now carefully define the notion of recursive logic programs. Then we
shall define the notion of proof schemes which will lead to the definitions of locally
finite programs. Finally we shall describe the extension of the Reiter's concept of
normal default theories to recursive logic programs following Marek, Nerode and
Remmel.
A program clause is an expression of the form
C = P<-gi,...,g n ,-T 1 ,...,-.r m (6.1)
115
where p,qi, . . . ,q n ,ri,. . . ,r m are atomic formulas in some propositional language C.
A program is a set of clauses of the form (6.1). A clause C is called a Horn clause if
m = 0. We let Horn(P) denote the set of all Horn clauses of P. H P is the Herbrand
base of P, that is, the set of all atomic formulas of the language of P.
If P is a program and M C H P is a subset of the Herbrand base, define
operator T PM :V{H P ) -* V{H P ) where T PM {I) is the set of all p such that there
exists a clause C = p «- ft,. . . ,^,-iTi -*•„, in P such that ft € /,. . . ,fc € /
and {r lr ..,r m }nM = 0.
The operator T P , M is a monotonic finitizable operator, see Apt (1990), and
hence possesses a least fixpoint F PM . Given program P and M C # P , the Gelfond-
Lifschitz reduct of P is defined as follows. For every clause C of P, execute the
following operation: If some atom a belongs to M and its negation ->a appears in C,
then eliminate C altogether. In the remaining clauses that have not been eliminated
by the operation above, eliminate all the negated atoms. The resulting program P$ L
is a Horn propositional program (possibly infinite). The program P$ L possesses a
least Herbrand model. If that least model of P° L coincides with M, then M is called
a stable model for P. Gelfond and Lifschitz (1998) proved the every stable model of
P is a minimal model of P and that M is stable model of P iff M = F P<M .
Having characterized stable models as fixpoints of (parametrized) operators,
consider the form of elements of F PyM . A P, M- derivation of an atom p is a sequence
(Pi, • • >tP$) such that (i) p s = p and (ii) for every i < s, either n p t «-" is a member
of P or there is a clause C = " Pi <- ft, ...,«,, -*i,. .. , -r m " such that C G P,
Qu---,q n 6 {Pii -.,ft-i} , and ri,..., r m £ M. It is easy to show that F PM is
the set of all atoms possessing a P, M-derivation. Thus M is a stable model of the
program P if and only if M consists exactly of those atoms which possess a P, M-
derivation.
116
The property that a sequence (p l5 . . . ,p s ) is a P, M-derivation of an atom p
does not depend on the whole set M but only on the intersection of M and a certain
finite set of atoms that occur in the derivation. In order that the sequence (pi,...,p s )
be a P, M-derivation of an atom p s , some atoms must be left out of the set M. Each
derivation depends on a finite number of such omitted atoms. In other words, if we
classify the atoms according to whether they are "in" or "out" of M, the property
that a sequence (pi,...,p,) is a P, M-derivation depends only on whether a finite
number of elements are out of M. The notion of a proof scheme formalizes this idea.
A (P-)proof scheme for an atom p is a sequence S = {(p u Ci,Ui)) s i=l of triples
such that for each triple (p t , Q, U { ), p { E H P , d e P is a clause with the head p % and
Ui is a finite subset of H P . Such sequence S is a proof scheme for p if (1) p, = p, and
for every i (2) Q = p % <- q h ... ,q n , ir u ..., -.r m , where {q l ,...,q n } C {pi t ...p i - 1 }
and Ui =Ui-i U{r u ...,r m }.
We call p the conclusion of 5, written p = cln(S), and the set U, the support of
5, written supp(S). We say that a subset M C H P admits a proof scheme S =
((ft,C il C/ t ))LiifMn[/ s = 0.
The following proposition due to Marek, Nerode,and Remmel in [MNR90]
characterizes stable models in terms of the existence of proof schemes.
Proposition 6.4.93 Let M C H P . Then M is a stable model of P if and only if
(1) for every pe M, there is a proof scheme S for p such that M admits S, and
(2) for every pi M, there is no proof scheme S for p such that M admits S.
As stated in the introduction, restrictions on the number of proof schemes
greatly reduce the possible complexity of the set of stable models of a recursive logic
program P. But how many derivation schemes for an atom p can there be? If we
allow P to be infinite, then it is easy to construct an example with infinitely many
derivations of a single atom. Moreover given two proof schemes, one can insert one
117
into the other (increasing appropriately the sets Ui in this process, with obvious
restrictions). Thus various clauses C { may be immaterial to the purpose of deriving
p. This leads us to introduce a natural relation -< on proof schemes using a well-
known device from proof theory. Namely, we define Si -< S 2 if Si , S 2 have the same
conclusion and if every clause appearing in Si also appears in S 2 . Then a minimal
proof scheme for p is defined to be a proof scheme S for p such that whenever S' is a
proof scheme for p and S' -< S, then S -< S'. Note that -< is reflexive and transitive,
but -< is not antisymmetric. However it is wellfounded. That is, given any proof
scheme S , there is an S' such that S' -< S and for every S", if S" -< S', then S' -< S".
Moreover, the associated equivalence relation, S = S', defined by S -< S' and S' -< S,
has finite equivalence classes.
Example 6.4.32 Let Pi be the following program:
C x : p(0)<-^q{Y).
C 2 : nat(0) <- .
C 3 : nat(s(X)) <- nat{X).
Then atom p(0) possesses infinitely many minimal proof schemes. For instance,
each one-element sequence Si = ((p(0), Ci0j, {s^O)})) where 6 t is the operation of
substituting s l (0) for Y , is a minimal proof scheme for p(0). However if program P 2
is the result of replacing clause C\ by
C[: q ( s (Y))^^q(Y),
each atom possesses only finitely many minimal proof schemes.
We shall call a program P locally finite if for every atom p, there are only
finitely many minimal proof schemes with conclusion p. If P is locally finite and
p G H P , we let D p denote the union of all supports of minimal proof schemes of p.
Clearly for any M C H P , the question of whether p has a P, M-derivation depends
only onMflDp. This implies that if P is locally finite, when we attempt to construct
118
a subset M C H P which is a stable model for P, we can apply a straightforward
(although still infinite) tree construction to produce such an M, if such an M exists
at all.
Next, we need to make the notion of a recursive program precise. First, assume
that we have a Godel numbering of the elements of the Herbrand base H P . Thus,
we can think of each element of the Herbrand base as a natural number. U p € H P ,
write c(p) for the code or Godel number of p. Let u = {0, 1,2,.. .}. Assume [,]
is a fixed recursive pairing function which maps w x uj onto u> which has recursive
projection functions *, and 7r 2 , defined by ni([x u x 2 }) = x { for all x 1 and x 2 and i e
{1,2}. Code a finite sequence (x u . . . , x n ) for n > 3 by the usual inductive definition
[x 1 ,...,x n } = [xi, [x 2 , . . . ,x n }}. Next, code finite subsets of a; via "canonical indices".
The canonical index of the empty set, 0, is the number and the canonical index of a
nonempty set {x , ..., x n }, where x Q < . . . < x n , is ££_, 2 X * . Let F k denote the finite
set whose canonical index is k. Once finite sets and sequences of natural numbers
have been coded, we can code more complex objects such as clauses, proof schemes,
etc. as follows. Let the code c(C) of a clause C = p <r- q u . . . , q n , -r u -rr m be
[c(p), k, I], where k is the canonical index of the finite set {c(ft), . . . , c(q n )}, and I is
the canonical index of the finite set {c( ri ), ..., c(r m )}. Similarly, let the code c(S) of a
proof scheme S = ({p u Q, f/,))^ be [s, [[c( Pl ), c(d), c{U x )\, . . . , [c(p s ), c(C s ), c(U s )}]},
where for each i, c(Ui) is the canonical index of the finite set of codes of the elements of
Ui. The first coordinate of the code of a proof scheme is the length of the proof scheme.
Once we have defined the codes of proof schemes then for locally finite programs we
can define the code of the set D p consisting of the union of the supports of all minimal
proof schemes for P. Finally we code recursive sets as natural numbers. Let <f> , &, . . .
be an effective list of all partial recursive functions where <t> e is the partial recursive
function computed by the e-th Turing machine. By definition, a (recursive) index
of a recursive set R is an e such that <j) e is the characteristic function of R. Call
119
a program P recursive if the set of codes of the Herbrand universe Hp is recursive
and the set of codes of the clauses of the program P is recursive. If P is a recursive
program, then by an index of P we mean the code of a pair [u, p] where u is an index
of the recursive set of all codes of elements in Hp and p is an index of the recursive
set of the codes of all clauses in P.
For the rest of this disscusion we shall identify an object with its code as
described above. This means that we shall think of the Herbrand universe of a
program, and the program itself, as subsets of u and clauses, and proof schemes as
elements of a;.
We also need to define various types of recursive trees and n° classes. Let uo <u
be the set of all finite sequences from u> and let 2 <u ' be the set of all finite sequences
of O's and l's. Given a = (c*i, . . . , a n ) and (3 - (ft, . . . , k ) in u; <w , write a Q (3 if
a is initial segment of ft i.e. , if n < k and ojj = fa for i < n. In this paper, we
identify each finite sequence a = (cti, . . . , a n ) with its code c(a) = [n, [c*i, . . . , a n ]] in
Uf. Let be the code of the empty sequence 0. When we say that a set S C u <UJ is
recursive, recursively enumerable, etc., what we mean is that the set {c(a):a 6 5}
is recursive, recursively enumerable, etc. Define a tree T to be a nonempty subset
of lu <uj such that T is closed under initial segments. Call a function f:u — > u> an
infinite path through T provided that for all n, (/(0), . . . , /(n)> € T. Let [T] be the
set of all infinite paths through T. Call a set A of functions a n^-class if there exists
a recursive predicate R such that A = {f:u -> u :Vn(R(n, [/(0), . . . , /(n)])}. Call a
Til-class A recursively bounded if there exists a recursive function g: u — > u such
that V/ G A\fn(f(n) < g(n)). It is not difficult to see that if A is a rij-class, then
A = [T] for some recursive tree T C uj <u} . A tree T C uj <u) is highly recursive if
T is a recursive finitely branching tree and also there is a recursive procedure which,
applied toa= (oi, ... , a n ) in T, produces a canonical index of the set of immediate
successors of a in T. Then if C is a recursively bounded flj-class, it is easy to show
120
that C = [T] for some highly recursive tree T C u <UJ , see CR98. For any set A C to,
the set A' = {e:<j>^{e) is defined} is called the jump of A, let 0' denote the jump
of the empty set 0. We write A <t B if A is Turing reducible to B and A = T B if
A < T B and B <t A. A function / : C -» D is said to be degree-preserving if
;4 =r /(4) for all A EC.
Even if F is a locally finite program, there is no guarantee that the global be-
havior of the function p t-¥ D p , mapping u> into u>, has any sort of effective properties.
Thus we are led to define the following.
We say that a locally finite recursive program F possesses a recursive proof
structure (rps) if (1) F is locally finite, and (2) the function p i-> D p is recursive. A
locally finite recursive program with an rps is called an rps program.
6.5 Equivalence of Logic Programming to Nonmonotonic Rule Systems
The equivalence of Logic Programming to Nonmonotonic Rule Systems has
been shown by Cenzer, Marek, Nerode, Remmel and others. Here, we give the
equivalence as shown by Cenzer and Remmel [CR99]. We shall encode now the stable
models of logic programs as extensions of suitably chosen nonmonotonic rule systems.
The universe of all our systems, U, will be the Herbrand base of the program. Next,
to every general propositional clause C,
C =p<r- q u ...,q m ,^r u ...,-^r n
assign the rule
9i,...,9m :ri,...,r„
re = •
P
Now, given the program F, define
Np = {r c : C 6 ground{P)}
We then have the following result
121
Theorem 6.5.94 Let P be a general logic program. Let M be a subset of the tier-
brand base of P. Then M is a stable model of P is and only if M is an extension of
the nonmonotonic rule system (U,Np).
Theorem 6.5.94 allows us to obtain results concerning stable models of logic programs
from theorems about extensions of nonmonotonic rule systems.
These theorems and other similar results obtained in mnr90a,mnr90b indicate
why nonmonotonic rule systems are useful in the investigations of various nonmono-
tonic logical formalisms. The results, both positive and, to some extent, negative,
on nonmonotonic rule systems provide us with corresponding results for all these
formalisms.
6.6 Previous Results Through the Eves of Logic Programming
In this section, we shall introduce the key notion of a locally determined logic
program P. The informal notion of a locally determined logic program P is one in
which the existence of a proof scheme for an atom a, (or the lack of existence thereof)
can be determined by examining only clauses or proof schemes involving some initial
segment of the Herbrand base of P. More formally, fix some countable logic program
P and some listing a Q , Oi, . . . of the atoms of Herbrand base of P without repetitions.
(We shall make the convention that if P is recursive logic program, then there is some
recursive function h such that h(i) = a { .) Then given a proof scheme or a clause </>,
we write max(<f)) for the max({i : a { occurs in 0}). We shall write P n for the set of
all clauses C e P such that max(C) < n and let A n = {a , . . . ,o»}.
Definition 6.6.95 We shall say that n is a level of P if for all S C {a , . . . ,a„}
and all i < n, whenever there exists a proof scheme ip such that cln{i>) = a t and
supp(tp)llS = 0, then there exists a proof scheme <p such that cln(4>) = a it supp{(j)) n
S = and max(<f>) < n. Note that by definition, the Herbrand base H Pn of P n is
contained in A„
122
Theorem 6.6.96 Suppose that n is a level of P and E is a stable model of P. Then
E n = E fl {a , . . . , a n } is a stable model of P n .
Proof: If E is a stable model of P, then for any a* G E n , there is a proof scheme ip
such that cln(ip) — aj and supp(ip) f) E = 0. Thus, in particular, supp(ip) n E n =
so that since n is a level, there exists a proof scheme <j> such that max((j)) < n,
cln(<(>) = a,, and supp{(j>) C\E n = $. Thus <£ is a proof scheme of P n and E n admits <f>.
Vice versa, if i < n and a* is not in £ n , then there can be no proof scheme <fi of P n
such that cln((j)) = a*, max(4>) < n, and supp((j)) fl £„ = since this would violate
the fact that E is a stable model of of P. Thus E n is a extension of P n .
Definition 6.6.97 1. We shall say that a logic program P is locally determined
if P is countable and there are infinitely many n such that n is a level of P.
2. Suppose that P is a recursive logic program. Then we say that P is effectively
locally determined if P is locally determined and there is a recursive function
f such that for all i, f(i) > i and f(i) is a level of P.
Notation: If P is locally determined, we let lev(P) — {n : n is a level of P}.
In [MNR90 and MNR92a], Marek, Nerode, and Remmel showed that the
problem of finding a stable model of a locally finite recursive logic program can be
reduced to finding an infinite path through a finitely branching recursive tree and
the problem of finding a stable model of a rsp logic program can be reduced to
finding an infinite path through a highly recursive tree. A locally determined logic
program is not always locally finite since it is possible that a given atom has infinitely
many proof schemes which involves arbitrarily large atoms. Vice versa, it is possible
to give examples of locally finite logic programs which are not locally determined.
Nevertheless, we shall see that we get similar results to those of Marek, Nerode,
and Remmel for locally determined and effectively locally determined recursive logic
programs.
123
Theorem 6.6.98 Let P be a recursive logic program.
1. If P is locally determined, then there is a recursive finitely branching tree T
and a 1:1 degree preserving correspondence between the set set of stable models
£ of P and [T] and
2. If P is effectively locally determined, then there is a highly recursive finitely
branching tree T and a 1:1 degree preserving correspondence between the set set
of stable models £ of P and [T] .
Proof:
There is no loss in generality in assuming that H p = u and that a = 0, ai =
1, Next observe that for each n, P n has only finitely many minimal proof schemes
so that we can effectively list all minimal proof schemes </> < fa < . . . in such a way
that
1. if max((f) k ) = i and max{(j)i) = j and i < j, then k < I. (This says that if i < j,
then the proof schemes whose max is i come before those proof schemes whose
max is j.)
2. ifmax((j) k ) = max(<t>{) = i, k < I if and only if c(<f> k ) < c{<j>i) where c{4>) denotes
the index assigned to a proof scheme <j> under our effective Godel numbering of
the proof schemes.
We shall encode a stable model M of P by a path * M = (xfc,*!,. . .) through
the complete ^-branching tree lj <uj as follows. First, for all i > 0, 7r 2i = xm(0- That
is, at the stage 2z we encode the information if i belongs to M. Next, if 7r 2i = then
7T2i+i = 0. But if 7r 2i = 1 so that i 6 M, then 7r 2l+ i = q M {i) where q M (i) is the least q
such cln((j) Q ) = i and supp{<j) q ) n M = 0. Thus </> 9mW is the least proof scheme which
shows that i € Fp <M .
124
Clearly M < T tt m since it is enough to look at the values of tt m at the even
levels to read off M. Now given an M-oracle, it should be clear that for each i £ M,
we can use an M-oracle to find 9m(0 effectively. This means that ty m < t M. Thus
the correspondence M h-> tx m is an effective degree-preserving correspondence. It is
trivially one-to-one.
Next we construct a recursive tree T C u u such that
[T] = {tte : E is a stable model of P}.
Let L k = max({i : max((j)i) < k}). It is easy to see that since P is a locally
determined recursive logic program, we can effectively calculate L k from A;. We have
to say which finite sequences belong to our tree T. To this end, given a sequence
a = (cr(0), . . . , a(k)) € w <UJ set l„ = {i : 2z < k A a(2i) = 1} and O a = {i : 2i <
k A a(2i) = 0}. Now we define T by putting a into T if and only if the following four
conditions are met:
(a) Vi(2? + 1 < k A a(2i) = => a(2i + 1) = 0).
(b) Vi(2? + 1 < k A cr(2z) =la> cr(2z + 1) = q where </>, is a minimal proof scheme
such that cln(<j) q ) = i and supp(<f) q ) n I a = 0).
(c) Vz(2z + 1 < k A cr(2i) = 1 => there is no c € L LJt/2 j such that dn(^ e ) = »,
supp((j) c ) C CT and c < <r(2i + 1)).
(here [-J is the so-called number-theoretic "floor" function).
(d) Vi(2i < k A tr(2i) = => there is no c e L Lfc/2 j such that c/n(c/> c ) = i and
supp((j) c ) C O ff ).
It is immediate that if a G T and r Qa, then r G T. Moreover it is clear from
the definition that T is a recursive subset of u <w '. Thus T is a recursive tree. Also,
it is easy to see that our definitions ensure that, for any stable E of P, the sequence
n B is a branch through T, that is, ir E G [T].
We shall show now that every infinite branch through T is of the form -n E for
a suitably chosen stable model E. To this end assume that /3 - (/?(0), /?(!), . . .) is
125
an infinite branch through T. There is only one candidate for E, namely E = {i ;
/3(2i) = 1}. Two items have to be checked, namely, (I) E$ is an stable model of P
and (II) 7r {Eg) = p.
To prove (I), first observe that if i e E , then a(2i) = 1 and o(2i + 1) = q
where (j) q is a proof scheme such that cln((j) q ) = i. Moreover condition (c) and the fact
that a n = (P , Pi, . . . , p n ) e T for all n > 2% + 1 easily imply that supp((p q ) n I„ n -
for all such n and hence supp((j) q ) D Ep = 0. In addition, condition (c) ensures that
<?!> g is the least proof scheme with this property. Similarly if i £ Ep, then condition
(d) and the fact that a n - {Po,Pi, . . . , P n ) € T for all n > 2i + 1 easily imply that
there can be no proof scheme (f> q with cln(<f) q ) = i and supp((j) q ) f\ Ep = %. It then
follows from Proposition 6.4.93 that Eg is a stable model of P and that 7r (£y3 ) =
The key fact needed to establish the branching properties of T is that for
any sequence a € T and any i, either a(2i) = a(2i + 1) = or a(2i) = 1 and
a(2i + 1) codes a minimal proof scheme for i. We just note that when a proof scheme
tp = a(2i + 1) does not correspond to a path tt e , then there will be some k such that
a has no extension in T of length k. This will happen once we either find a smaller
code for a proof scheme or we find some u > i in the support of rf> such that all
possible extensions r of a have t(2u) = 1.
We claim that T is always finitely branching and that if P is effectively locally
determined, then T is highly recursive. Clearly the only case of interest is when
2i + 1 < k and a(2i) = 1. In this case we will let a(2i + 1) = c where cln(<j) c ) = i and
supp((j) c ) n 7 a = and there is no a < c such that cln((j) a ) = i and supp((f) a ) (1 I a = 0.
Now suppose that p is level and i < p. Then by definition, there must be a minimal
proof scheme ip such that max(ip) < p, cln(tp) = i, and supp(ip) D I a = 0. Thus
tp = (j) q for some q < L p . It follows that c < L p where p is the least level greater
than or equal to i. Thus T is always finitely branching. Now if P is effectively locally
126
determined and this is witnessed by the recursive function /, then it will always be
the case that c < Lj^) so that T will be highly recursive.
Corollary 6.6.99 Suppose that P is a countable locally determined logic program
such that there are infinitely many n such that P n has a stable model E n . Then P
has a stable model.
Proof: Now consider the tree T constructed for P as in Theorem 6.6.98. Here we
again can construct our sequence of minimal proof schemes O , 0i, ■ • • recursive in P
just as we did in Theorem 6.6.98. However, we can only conclude that T is recursive
in P. Nevertheless, we are guaranteed that T is finitely branching which is all we
need for our argument.
Now fix some level n and consider some m>n such that P m has an extension
E m . Then by the exact same argument as in Theorem 6.6.96, E n = E m n {0, . . . , n}
will be a stable model of P n . Now consider the node a En = (ct(0), . . . , a(2n + 1)) such
that
1. a{2i) = l\fieE n and u(2i) = if i <$. E n ,
2. <7(2z + l) = 0if(7(2t) = 0, and
3. cr(2i + 1) = c where c is least number such that max((f> c ) < n, cln{<j) c ) = i, and
supp((f) c )r\E n = 0. (Note it follows from our ordering of minimal proof schemes
that <j> c is the least proof scheme <f> such that dn{<j>) = i and supp{<f>)C\E n - 0.)
It is easy to check that our construction of T ensures that a G T. It follows that T
is infinite finitely branching tree and hence T has infinite path -k by Konig's Lemma.
Our proof of Theorem 6.6.98 shows that E„ is an stable model of P.
We now give two conditions which ensure the existence of recursive stable
models.
127
Definition 6.6.100 1. Let P be a locally determined logic program and lev(P) =
{Iq < li < . . .} . Then we say say that P has the level extension property if
for all k, whenever E k is a stable model of Pi k , there exists a stable model E k+i
ofP ik+l such that E k+i n {a , ...,ai k } = E k .
2. A level n of P is a strong level of P if for any levels m < n of P and any stable
model E m of P m , if there is no stable model E of P with Er\{a , . . . , a m } = E m ,
then there is no stable model E n of P n with E n D {a , . . . , a m } = E m .
3. P has effectively strong levels if P has infinitely many strong levels and
there is a computable function f such that for each i, i < f(i) and f(i) is a
strong level.
In general, it is not easy to ensure that a locally determined logic program P
has the level extension property. However, there are many natural examples where
this condition is satisfied. One way to generate such programs is to consider the
following result from recursive combinatorics. Bean [be76] showed that there there
exists highly recursive connected graphs which are 3-colorable but not recursively
/c-colorable for any k. However Bean also showed that every infinite connected k-
colorable highly recursive graph G is recursively 2/c-colorable. Here a graph G =
(V, E) is highly recursive if the edge set V is a recursive subset of w, the set of codes of
the sets {x, y} G E is recursive, G is locally finite, i.e. the degree of any vertex v e V
is finite, and there is an effective procedure which given any vertex v eV produces a
code of N(x) = {y £V : {x,y} e E}. A recursive 2/c-coloring of G can be produced
as follows. Given any set W C V, let N(W) = {y G V - W : (3x e W)({x,y} e
E}. Then given any x 6 V, define an effective increasing sequence of finite sets
= A , Ai,Ai,... where Ai = N(x) U {x} and for all k > 1, A k = A k _ x U N{A k _ x ).
It is easy to see that there can be no edge from an element of A k to an element of
A k+ 2 - Ak+v Since G is A;-colorable, the induced graph determined by A { - A % _ x is
128
fc-colorable for alii > 1. We then defined a recursive 2/c-coloring of G as follows.
(Step 1) Find a coloring of A\ using colors {1, ... k},
(Step 2) Find a coloring of A 2 — Ai using colors {k + 1, . . . , 2k},
(Step 3) Find a coloring of A 3 - A - 2 using colors {1, . . . fc},
(Step 4) Find a coloring A± — A 3 using colors {k + 1 2A;}, etc.
One can easily write a logic program to implement this procedure and it will naturally
be effectively locally finite and have the level extension property.
Theorem 6.6.101 1. Suppose that P is an effectively locally determined recursive
logic program with the level extension property. Then for every level n and
stable model E n of P n , there is a recursive stable model of E of P such that
E(l{a ,...,a n } = E n .
2. Suppose that P is a recursive logic program with effectively strong levels. Then
for every level n and stable model E n of P n , if there is a stable model E of P
with E D {ao, . . . ,a n } = E n , then there is a recursive stable model of E of P
such that E n {a , . . . , a n } = E n .
Proof: For (1), fix a level n of P and a stable model E n of P. Suppose that /
is the function which witnesses the fact P is effectively locally determined. Then
let 60,61,62, ■•• be the sequence n,/(n),/(/(n)), . . .. It is easy to see that our
level extension property implies that we can effectively construct a sequence of sets
E bo ,E bl ,E b2 ,. . . such that (1) E bo = E n , (2) for all j > 0, E bj is a stable model of P b ,
and (3) for all j > 0, E bj+1 fl {a , . . . , a bj } = E bj . Now consider tree T and the nodes
a Eb as constructed in Corollary 6.6.99. It is easy to check that for all i, a Eb G T
and that a EbQ C a Ebi E a Eb2 E • • •• It follows that there is a unique path /3 in [T]
which extends all a Eb _ and that E = \J i>0 a Eb , is a stable model of P. Moreover E
is recursive because to decide if a, 6 E , one need only find k such that b k > j, in
which case, a ; e E <=> a, G CT£ 6 .
129
For (2), assume that / is the recursive function which witnesses the fact that P
has strong levels and let 6 , h, h, ■ ■ ■ be defined as above. We claim that the property
of strong levels once again lets us construct an effective sequence E bo ,E bi ,E b2 ,... such
that (1) E bo = E n , (2) for all j > 0, E bj is a stable model of P bj , and (3) for all j > 0,
E bj+l n {a Q ,...,a bj } = E bj . That is, suppose that we have constructed E bk such
that there exists a stable model S of P such that S D {a , . . . ,a bk } = E bk . Now
consider the strong level b k+2 . Our definition of strong level ensures that there must
be some stable model F k+2 of P h+2 such that F k+2 D {a , . . . , a bk } = E bk . Then let
Eb k+1 = Fk+2 n {°o, • ■ • , a b k+i }- The argument in Theorem 6.6.96 shows that E bk+l is
a stable model of P bk+l . Moreover, since b k+2 is a strong level, there must be a stable
model 5' of P such that E bk+l = S' D {a , . . . , a bk+1 } since otherwise, there can be no
extension F of P bk+2 such that E bk+1 = F n {a , . . . , a bk+1 }. This given, we can then
construct our desired recursive stable model E exactly as in (1).
We now consider another, more direct approach to producing a recursive stable
model.
Definition 6.6.102 We say that a recursive logic program P has witnesses with
effective delay if there is a recursive function f such that for all n, f(n) > n
and whenever there is a set S C {a Q ,...,a n } such that there is a stable model E
of P with E fi {a , ...,a n } = Sbut there is no stable model F of U such that F n
{ao, . . . , a n , a n+ i} = S, then either
(i) there is a proof scheme <f> with max(<f>) < n + 1 such that cln(cj)) = a n+l and
supp{(j)) C {a ,...,a n } - S, or
(ii) for all sets T included in {a n+2 , . . . ,a /(n) }, there is a proof scheme ip T with
max(ip) < f(n) such that supp(xjj T ) C {a , . . . , a /H } - (T U S) and
dn{ipr) e {a , . . . , o /(n) } -(Tu5).
130
Note that in case (i), the proof scheme 4> witnesses that we must have a n+1 in any
stable model E such that E n {a , . . . ,a n } = S. In case (ii), the proof schemes <j) T
show that we can not have a stable model E of P such that E D {a , . • • , a/ (n) } =
S U T so that we are again forced to have a„ +1 in any stable model E such that
£n{a ,...,a n } = S.
Theorem 6.6.103 Suppose that P is a recursive logic program which has witnesses
with effective delay and has at least one stable model. Then the lexicographically least
stable model E of P is recursive.
Proof: We can construct the lexicographically least stable model E of P by
induction as follows.
Suppose that for any given n we have constructed E n = E n {a , . . . ,a„}. Then
E n +\ = E n unless either
(i) there is a proof scheme <j) of level n such that supp(<j)) C {a , ...,a n } - E n and
cln((j)) = a n+1 or
(ii) for all sets T included in {a n+2 , . . . ,a /(n) }, there is a proof scheme ip T with
maxifo) < f(n) such that supper) C {a , . . . , a /(n) } - (T U .£„) and
cin(^r) 6 {a , . . . , a /{n) } - (TU ^„).
in which case £ n+1 = £ n U {a n+1 }. Note that since there are only finitely many
minimal proof schemes <j) with max(4>) < k for any given k, we can check conditions
(i) and (ii) effectively. Since there is a stable model, it is easy to see that our
definitions insure that E n is always contained in the lexicographically least stable
model of P. Thus E = \J n E n is recursive.
By putting suitable effective bounds on the effective levels and/or the witnesses
with effective delay, one can readily come up with conditions that force P to have
exponential time, NP, or P-time stable models.
CHAPTER 7
FUTURE DIRECTIONS
There are many avenues of research yet to be explored in Nonmonotonic Rule
Systems and other forms of Nonmonotonic Logic, including Default Logic and Logic
Programming. As far as common derivations are concerned, we have only scratched
the surface. There are three extensions of the research which should be followed,
namely further work in the complexity of the common derivation, applications of the
current results, and combining Nonmonotonic Rule Systems with Fuzzy Logic and/or
Multiple- Valued Logic.
The complexity of the common derivations have been touched upon in this
dissertation, but have been by no means exhaustively studied. In addition, we might
consider a multitude of other types of complexity aside from those mentioned here.
Some of the original motivation for the results in this dissertation was to create
the mathematics necessary to apply Nonmonotonic Logic to such areas as advertising,
political campaigning, and other social sciences. The results, at this point, I believe
are sufficient to begin the creation of models for use in these fields. As a matter of
practicality, these models should be included in the future directions of this research.
To combine Nonmonotonic Rule Systems with Fuzzy Logic and/or Multiple-
Valued Logic may seem a strange or unrelated road to follow from the present work.
However, Nonmonotonic Logic was initially established with the intention of formal-
izing human reasoning. It is optimistic in the least to suppose that every human
belief and thought carries a black-and-white value of true or false. Human reason-
ing often treads a grey area somewhere in between. Thus, Fuzzy Logic or at least
Multiple- Valued logic is called for. In Nonmonotonic Rule Systems we may use any
131
132
underlying logical system to govern U. Interesting results may first be found in the
comparitively less complicated world of Multiple- Valued Logic, begining with three
values and generalizing results to n-valued logic. From there, choosing Fuzzy Logic
to be the "logic of choice" for the Nonmonotonic Rule System < U,N > would be
the natural step to take.
This is by no means a complete list of possible future directions. Nonmono-
tonic Logic, a vigorous and rapidly growing area of research, is still in its infancy.
There are many questions still to be answered, and each new result brings its weight
in new roads to follow.
REFERENCES
[AN78] H. Andreka, and I. Nemeti. The Generalized completeness of horn predi-
cate logic as a programming language. Acta Cybernetica 4(1978): 3-10.
[Apt90] K.R. Apt. Logic programming. Handbook of theoretical computer science,
J. van Leeuven, (ed.). Cambridge, MA: MIT Press, 1990.
[AB90] K.R. Apt, and H.A. Blair. Arithmetical classification of perfect models
of stratified programs. Fundamenta Informaticae 13 (1990): 1-17.
[B90] J. Banks. A model of electoral competition with incomplete information.
Journal of Economic Theory 50 (1990): 309-325.
[Be76] D.R. Bean. Effective coloration. Journal of Symbolic Logic 41 (1976): 469-
480.
[BDK97] G. Brewka, J. Dix, and K. Konolige. Nonmonotonic reasoning: An
overview. Stanford, CA: CSLI, 1997.
[BG97] G. Brewka, and G. Gottlob. 1997. Well-founded semantics for default
logic. Fundamenta Informaticae 31(3-4) (1997): 221-236.
[CMMT95] P. Cholewihski, W. Marek, A. Mikitiuk, and M. Trusczcyhski. Exper-
imenting with nonmonotonic reasoning. Proceedings of the Twelfth In-
ternational Conference on Logic Programming 267-281. Cambridge, MA:
MIT Press, 1995.
[CMT96] P. Cholewihski, W. Marek, and M. Trusczcyhski. Default reasoning sys-
tem DeRes. Proceedings of the International Conference on Principles
of Knowledge Representation and Reasoning, L. Carlucci Aiello, J. Doyle
and S. Shapiro (eds.). KR96 (1996): 518-528.
[CR98] D. Cenzer and J.B. Remmel. ITj'-classes in mathematics. Handbook of
recursive mathematics: Volume 2, Yu. L. Ershov, S.S. Goncharov, A.
Nerode, and J.B. Remmel (eds.). Studies in Logic and the Foundations
of Mathematics, 139: 623-822. Amsterdam: Elsevier, 1998.
[CR99] D. Cenzer, and J. Remmel. Complexity, decidability, and completness.
Preprint.
[CRV99] D. Cenzer, J.B. Remmel, and A.K.C.S. Vanderbilt. Locally determined
logic programs. Proceedings of the 5th international Conference on
Logic Programming and Nonmonotonic Reasoning (LPNMR99). Berlin:
Springer- Verlag, 34-49. 1999.
[Do79] J. Doyle A truth maintenance system. Artificial Intelligence 12 (1979):
231-272.
133
134
[DM82] J. Doyle and D. McDermott. Nonmonotonic logic II: nonmonotonic modal
theories. Journal of the A.C.M. 29 (1982): 33-57.
[EG93] T. Eiter, and G. Gottlob. Complexity results for disjunctive logic pro-
gramming and application to nonmonotonic logics. Proceedings of the
Tenth International Logic Programming Symposium (ILPS-93). Cam-
bridge, MA: MIT Press, 1993, 266-278. "
[EMTT96] J. Engelfriet, W. Marek, J. Treur, and M. Truszczyriski. Infmitary de-
fault logic for specification of nonmonotonic reasoning. Logics in Artificial
Intelligence, Proceedings European Workshop on Logics in Artificial In-
telligence, JELIA'96. Lecture notes in Artificial Intelligence 1126 (1996):
224-236.
[GL88] M. Gelfond and V. Lifschitz. The stable semantics for logic programs.
Proceedings of the 5th International Symposium on Logic Programming.
Cambridge, MA: MIT Press, 1988, 1070-1080.
[Gol94] C. Goldburg. The accuracy of game theory predictions for political be-
havior: cumulative voting in illinois revisited. Journal of Politics 56(4)
(1994): 885-900.
[Got92] G. Gottlob. Complexity results for nonmonotonic logics. Journal of Logic
and Computation 2(3) (1992): 397-425.
[Got93] G. Gottlob. Recent complexity results in logic programming and non-
monotonic reasoning and why they matter. Proceedings of the Second
International Workshop on Logic Programming and Nonmonotonic Rea-
soning LPNMR'93. Cambridge, MA: MIT Press, 1993, 265.
[Got95] G. Gottlob. The complexity of default reasoning under the stationary
fixed point semantics. Information and Computation 121(1) (1995): 81-
- * _ .
[GM94] G. Gottlob, and Z. Mingyi. Cumulative default logic: finite characteriza-
tion, algorithims and complexity. Artificial Intelligence 69 (1994): 329-
[MNR90] W. Marek, A. Nerode, and J. Remmel. A theory of nonmonotonic rule
systems I. Annals of Mathematics and Artificial Intelliqence 1 (1990):
241-273.
[MNR92a] W. Marek, A. Nerode, and J. Remmel. A theory of nonmonotonic rule
systems II. Annals of Mathematics and Artificial Intelliqence 51 (1992):
229-263.
[MNR92b] W. Marek, A. Nerode, and J. Remmel. How complicated is the set of
stabile models of a recursive logic program? Annals of Mathematics and
Artificial Intelligence 56 (1992): 119-135.
[MNR92c] W. Marek, A. Nerode, J. Remmel. The stable models of a predicate
logic program. Journal of Logic Programming 21(3) (1992): 129-154.
[MNR94] W. Marek, A. Nerode, and J. Remmel. A context for belief revision:
forward chaining-normal nonmonotonic rule systems. Annals of Pure and
Applied Logic 67(1-3) (1994): 269-323.
135
[MNR94a] W. Marek, A. Nerode, and J. B. Remmel. The stable models of predicate
logic programs. Journal of Logic Programming 21 (1994): 129-154.
[MNR95] W. Marek, A. Nerode, and J. Remmel. Complexity of normal default
logic and related modes of nonmonotonic reasoning. Proceedings of the
10th Annual IEEE Symposium on Logic in Computer Science Cambridge,
MA: MIT Press (1995): 178-187.
[MNR97a] W. Marek, A. Nerode, and J. Remmel. Complexity of recursive normal
default logic. Fundamenta Informaticae 32(2) (1997): 139-148.
[MNR97b] W. Marek, A. Nerode, and J. Remmel. Nonmonotonic rule systems
with recursive sets of restraints. Archivfur Mathematische Logik36 (1997):
339-384.
[MNR99a] W. Marek, A. Nerode, and J. Remmel. Logic programs, well-orderings
and forward chaining. Annals of Pure and Applied Logic 96 (1999): 231-
276.
[MNR99b] W. Marek, A. Nerode, and J. Remmel. Forward chaining-normal non-
monotonic rule systems. Preprint. 1999.
[MS89] W. Marek, and V. S. Subrahmanian. Relationship between logic program
semantics and nonmonotonic reasoning. Proceedings of the Sixth Inter-
national Conference on Logic Programming. Cambridge, MA: MIT Press
(1989), 417-419.
[MST91] W. Marek, G. Schwartz, and M. Truszczyhski. Ranges of strong nonmono-
tonic logics. Nonmonotonic Logic and Inductive Logic. Springer Lecture
Notes in Computer Science 543 (1991): 85-99.
[MT89a] W. Marek and M. Truszczyhski. Stable semantics for logic programs
and default theories. Proceedings of North American Conference on Logic
Programming. Cambridge, MA: MIT Press (1989), 243-256.
[MT89b] W. Marek and M. Truszczyhski. Relating autoepistemic and default log-
ics. Proceedings of the International Conference on Knowledge Represen-
tation KR89, San Fransisco, CA: Morgan-Kaufman (1989), 276-288.
[MT90] W. Marek and M. Truszczyhski. Modal logic for default reasoning. Annals
of Mathematics and Artificial Intelligence 1 (1990): 275-302.
[MT92] W. Marek and M. Truszczyhski. More on modal aspects of default logic.
Fundamenta Informaticae 17(1-2) (1992): 99-116.
[MT93a] W. Marek and M. Truszczyhski. Nonmonotonic logics; context-dependent
reasoning. Berlin: Springer- Verlag, 1993.
[MT93b] W. Marek and M. Truszczyhski. Normal form results for default logic,
nonmonotonic and inductive logic II. Springer Lecture Notes in Computer
Science, G. Brewka, K. P. Jandtke, and P. H. Schmitt (eds.), 659 (1993):
270-283.
[MTT97] W. Marek, J. Treur, and M. Truszczyhski. Representation theory for
default logic. Annals of Mathematics and Artificial Intelligence 21 (1997):
343-358.
136
[MZ90] W. Marek, and A. Zhang. On the classification and existence of structures
in default logic. Fundamenta Informaticae 13(4) (1990): 485-499.
[Rei80] R. Reiter. A logic for default reasoning. Artificial Intelligence, 13 (1980):
81-132.
BIOGRAPHICAL SKETCH
Amy K. C. S. Vanderbilt was born Amy Kathryn Colleen Sartain on February
17, 1975, in Fayetteville, Tennessee. She moved to Orlando, Florida, in 1978 where
she lived until 1992 and attended Lake Highland Preparatory School. In 1992 she
moved to Gainesville, Florida, to attend the Univeristy of Florida earning a bachelor's
degree in mathematics in 1995, a master's degree in pure mathematics in 1997 and a
doctorate in mathematics, specializing in logic, in May of 2000.
137
I certify that I have read this study and that in my opinion it conforms to
acceptable standards of scholarly presentation and is fully adequate, in scope and quality,
as a dissertation for the degree of Doctor of Philosophy.
^1_£
j£
?*g£4L
Douglas A. Cenzer, Chairman
Professor of Mathematics
I certify that I have read this study and that in my opinion it conforms to
acceptable standards of scholarly presentation and is fully adequate, in scope and quality,
as a dissertation for the degree of Doctor of Philosophy.
■^7^. [A' <7"^-C^-<r*-^
Jean A. Larson
Professor of Mathematics
I certify that I have read this study and that in my opinion it conforms to
acceptable standards of scholarly presentation and is fully adequate, in scope and quality,
as a dissertation for the degree of Doctor of Philosophy.
-tK^L
Rick L. Smith
Associate Professor of Mathematics
I certify that I have read this study and that in my opinion it conforms to
acceptable standards of scholarly presentation and is fully adequate, in scope and quality,
as a dissertation for the degree of Doctor of Philosophy.
O
Jorge Martinez
Professor of Mathematics
I certify that I have read this study and that in my opinion it conforms to
acceptable standards of scholarly presentation and is fully adequate, in scope and quality,
as a dissertation for the degree of Doctor of Philosophy.
Beverly A. Sanders
Associate Professor of Computer and
Information Science and Engineerng
This dissertation was submitted to the Graduate Faculty of the Department of
Mathematics in the College of Liberal Arts and Sciences and to the Graduate School and
was accepted as partial fulfillment of the requirements for the degree of Doctor of
Philosophy.
May 2000 Dean, Graduate School
LD
- .
1
20 CL
t \lW
UNIVERSITY OF FLORIDA
3 1262 08555 3393